proposition: Lemma Ech_powerset_prop c (m := slength c)(c':= Ech_powerset c): echelon c -> \0c <c m -> [/\ echelon c', slength c' = csucc m, esize c' = esize c, Vg c' m = J m \0c & forall k, k <c m -> Vg c' k = Vg c k].
proof: Proof. move => sa sb. move: (esize_prop1 sa sb) => sc. move: sa => [[[qa qb] sa2] sa3]. have ra: sub (range c') (Nat \times Nat). rewrite range_setU1 => i/setU1_P; case; first by apply: sa2. move => ->; apply: setXp_i => //; apply:NS0. have rb: ~ inc (slength c) (domain c). by apply:ordinal_irreflexive; apply: OS_nat. have dc1: domain c' = osucc (domain c) by rewrite domain_setU1. have dc2: domain c' = csucc (domain c) by rewrite (succ_of_nat qb). have lc: slistp c'. split; [ apply:(fgraph_setU1 _ qa rb) | rewrite dc2; fprops]. have ec:echelon c'. split => // i; rewrite /slength dc2; move/(cltSleP qb) => /cle_eqVlt []. move => ->; rewrite (setU1_V_out _ qa rb); saw. move =>_ ; split; [ by apply/cge1P | apply:cleR; fprops]. done. move => li; rewrite (setU1_V_in _ qa rb); first by apply: sa3. by apply /(NltP qb). have dc3: slength c' = csucc m by done. have sep: \0c <c slength c'. by rewrite /slength dc2; apply: succ_positive. have atval: Vg c' m = J m \0c by rewrite (setU1_V_out _ qa rb). have inval: forall k, k <c m -> Vg c' k = Vg c k. by move => k lkm; rewrite (setU1_V_in _ qa rb) //; apply /(NltP qb). move: sc=> [kN kp [j ja jb]] kd. split => //. apply:(esize_prop2 ec). exists j; first by rewrite /slength dc2; exact:(clt_leT ja (cleS qb)). by rewrite inval. move => i; rewrite /slength dc2; move/(cltSleP qb) => /cle_eqVlt []. move => ->; rewrite atval; aw => _; apply: (proj1 kp). by move => idc; rewrite inval //; apply: kd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)