proposition: Lemma Eextension_prop_id c f (g := echelon_extension c f) (is_identity := fun z => z = identity (source z)): echelon c -> (forall i, i <c esize c -> is_identity (Vg f i)) -> forall i, i <c slength c -> is_identity (Vg g i).
proof: Proof. move => ha hc i im. move: (slength_nat (proj1 (proj1 ha))) => mN. have iN:= (NS_lt_nat im mN); move: i iN im. have Hb x: is_identity (identity x) by rewrite /is_identity; aw. apply: Nat_induction1 => k kN Hr lkn. move: (Eextension_prop f ha lkn); simpl;set a := P _; set b := Q _. move => [pa pb pc]. case (p_or_not_p (a = \0c)) => az. move: (pa az) => [/cge1P ra rb ->]. apply: (hc _(cpred_pr0 ra rb (NS_esize ha))). case (p_or_not_p (b = \0c)) => bz. move: (pb bz) => [ra rb ->]. move:(cpred_pr6' kN ra rb) =>[qa qb qc]. move: (Hr _ qc (clt_ltT qc lkn)); rewrite /Vl -/g => ->. by rewrite etp_identity; apply: Hb. move:(pc az bz) => [ra rb rc rd ->]. move:(cpred_pr6' kN ra rb) (cpred_pr6' kN rc rd)=>[qa qb qc][qa' qb' qc']. move:(Hr _ qc (clt_ltT qc lkn)) (Hr _ qc' (clt_ltT qc' lkn)) => i1 i2. rewrite -/g /Vl i1 i2 ext_to_prod_identity; apply: Hb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)