proposition: Lemma Eextension_prop c f i (m := slength c)(g := echelon_extension c f) (n:= esize c): echelon c -> i <c m -> let a:= P (Vg c i) in let b := Q (Vg c i) in [/\ a = \0c -> [/\ \1c <=c b, b <=c n & Vg g i = (Vl f b)], b = \0c -> [/\ \1c <=c a, a <=c i & Vg g i = \Pof (Vl g a) ] & a <> \0c -> b <> \0c -> [/\ \1c <=c a, a <=c i, \1c <=c b, b <=c i & Vg g i = (Vl g a) \ftimes (Vl g b)]].
proof: Proof. by move => h; apply:erecdef_prop2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)