Numbers/nat_compl.v

@@ -302,6 +302,11 @@ Lemma nat_sub2_r :
   forall m n, (n <= m)%coq_nat -> (m - (m - n)%coq_nat)%coq_nat = n.
 Proof. lia. Qed.
 
+Lemma nat_sub_r_monot :
+  forall m n p, (m <= p)%coq_nat -> (n <= p)%coq_nat ->
+    (m < n)%coq_nat -> ((p - n)%coq_nat < (p - m)%coq_nat)%coq_nat.
+Proof. lia. Qed.
+
 Lemma nat_double_S : forall n, (2 * n.+1)%coq_nat = (2 * n)%coq_nat.+2.
 Proof. intros; rewrite Nat.mul_succ_r; apply nat_add_2_r. Qed.
 

Subsets/Finite_family.v

@@ -4413,10 +4413,13 @@ Lemma insertF_revF :
   forall {n} i0 x0 (A : 'E^n),
     insertF i0 x0 (revF A) = revF (insertF (rev_ord i0) x0 A).
 Proof.
-intros; rewrite (insertF_permutF rev_ord_inj). unfold revF.
-
-
-Admitted.
+intros n i0 x0 A; rewrite (insertF_permutF rev_ord_inj); unfold revF.
+extF i; rewrite !permutF_correct; destruct (ord_eq_dec i i0) as [-> | Hi].
+rewrite insert_f_ord_correct_l// !insertF_correct_l//.
+move: (skip_ord_correct_m i0) (inj_contra rev_ord_inj _ _ Hi) => H1 H2.
+rewrite insert_f_ord_correct_r !insertF_correct_r
+    insert_skip_ord rev_insert_ord; easy.
+Qed.
 
 Lemma revF_insertF :
   forall {n} i0 x0 (A : 'E^n),

Subsets/ord_compl.v

@@ -2431,6 +2431,26 @@ Proof. intros; apply injF_surj, rev_ord_inj. Qed.
 Lemma rev_ord_max : forall {n}, rev_ord (@ord_max n) = ord0.
 Proof. intros; apply ord_inj; simpl; apply subnn. Qed.
 
+Lemma rev_ord_monot :
+  forall {n} {i j : 'I_n}, (i < j)%coq_nat -> (rev_ord j < rev_ord i)%coq_nat.
+Proof.
+move=>> H; rewrite !rev_ord_correct -minusE; apply nat_sub_r_monot;
+    [apply /leP.. | rewrite -Nat.succ_lt_mono]; easy.
+Qed.
+
+Lemma rev_insert_ord :
+  forall {n} {i0 i : 'I_n.+1} (H1 : i <> i0) (H2 : rev_ord i <> rev_ord i0),
+    rev_ord (insert_ord H1) = insert_ord H2.
+Proof.
+intros n i0 i H1 H2; destruct (lt_eq_lt_dec i i0) as [[H3 | H3] | H3];
+    [| contradict H1; apply ord_inj; easy |];
+    move: (rev_ord_monot H3) => H4.
+rewrite insert_ord_correct_l insert_ord_correct_r; apply ord_inj; simpl.
+rewrite -minusE; lia.
+rewrite insert_ord_correct_r insert_ord_correct_l; apply ord_inj; simpl.
+rewrite -minusE; lia.
+Qed.
+
 Lemma cast_f_rev_ord :
   forall {n1 n2} (H : n1 = n2), cast_f_ord H (@rev_ord n1) = @rev_ord n2.
 Proof. intros; subst; fun_ext; apply ord_inj; easy. Qed.