proposition: Lemma erecdef_prop2 c (m := slength c)(f := echelon_recdef c) (n:= esize c): echelon c -> forall i, 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 = (h1 b)], b = \0c -> [/\ \1c <=c a, a <=c i & Vg f i = h2 (Vl f a) ] & a <> \0c -> b <> \0c -> [/\ \1c <=c a, a <=c i, \1c <=c b, b <=c i & Vg f i = h3 (Vl f a) (Vl f b)]].
proof: Proof. move => ec i lim ; move: (erecdef_prop ec); rewrite -/f. move => [ha hb hc] /=; rewrite (hc _ lim) /erecdef_combine. move: (esize_prop1 ec (cle_ltT (cle0x (proj31_1 lim)) lim)). rewrite -/n -/m; move=> [na nb nc nd]. move: ((proj2 ec) _ lim); simpl;set a := P _; set b := Q _; move=> [ia ib]. have hu: b = \0c -> a <> \0c. by move => bz az; move:(proj1 (ia bz)); rewrite az=> w; case:(cltNge clt_01). split. - move=> az; rewrite az; Ytac0. by have bn:=(nd _ lim az); split =>//; apply: (cge1 (proj31 bn)) => /hu. - by move => bz; move:(ia bz) (hu bz) => [a1 a2] a3; split => //;Ytac0; Ytac0. - move => az bz; move:(ib bz az) => [[q1 q2][q3 q4]]. by split => //; Ytac0; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)