proposition: Lemma echelon_value_prop c E i (m := slength c)(f := echelon_value c E) (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 f i = (Vl E b)], b = \0c -> [/\ \1c <=c a, a <=c i & Vg f i = \Po (Vl f a) ] & a <> \0c -> b <> \0c -> [/\ \1c <=c a, a <=c i, \1c <=c b, b <=c i & Vg f i = (Vl f a) \times (Vl f b)]].
proof: Proof. by move => h; apply:erecdef_prop2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)