proposition: Lemma Eextension_prop_bij_inv c f (g := echelon_extension c f) (lif := Lg (esize c) (fun z => inverse_fun (Vg f z))) (lig := echelon_extension c lif): echelon c -> (forall i, i <c (esize c) -> bijection (Vg f i)) -> forall i, i <c (slength c) -> bijection (Vg g i) /\ inverse_fun (Vg g i) = Vg lig 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 nN:=(NS_esize ha). apply: Nat_induction1 => k kN Hr lkn. move: (Eextension_prop f ha lkn) (Eextension_prop lif ha lkn). simpl;set a := P _; set b := Q _. move => [pa pb pc] [pa' pb' pc']. case (p_or_not_p (a = \0c)) => az. move: (pa az) (pa' az)=> [/cge1P ra rb ->] [_ _ ->]. have aux:= (cpred_pr0 ra rb (NS_esize ha)). by split; [ apply: (hc _ aux) | rewrite /Vl /lif LgV//; apply /(NltP nN)]. case (p_or_not_p (b = \0c)) => bz. move: (pb bz)(pb' bz) => [ra rb ->][_ _ ->]. move:(cpred_pr6' kN ra rb) =>[qa qb qc]. move: (Hr _ qc (clt_ltT qc lkn)) => [sa sb]. by move:(etp_inv sa) => [sc sd]; split => //; rewrite /Vl sd sb. move:(pc az bz) (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)). move => [b1 i1][b2 i2];split; first by exact : (ext_to_prod_fb b1 b2). by rewrite (ext_to_prod_inverse b1 b2) // i1 i2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)