proposition: Lemma erecdef_prop1 c: echelon c -> echelon_recdef_prop c (erecdef_combine h1 h2 h3).
proof: Proof. move => [[ka kb] kc] g1 g2 i lim Hr. rewrite /erecdef_combine. move: (proj2 ka) => mN. have iN:= (NS_lt_nat lim mN). have aux x: ech_good x i -> (Vl g1 x) = (Vl g2 x). move => [/cge1P ra' rb']; apply: Hr. have xN:=(NS_le_nat rb' iN). have [cpN cpv]:= (cpred_pr xN (nesym (proj2 ra'))). by apply/(cleSltP cpN); rewrite - cpv. move:(kc _ lim) => [kc1 kc2]. case: (p_or_not_p (P (Vg c i) = \0c)) => ca; Ytac0; Ytac0; first by done. case: (p_or_not_p (Q (Vg c i) = \0c)) => cb; Ytac0; Ytac0. by rewrite (aux _ (kc1 cb)). by move: (kc2 cb ca) => [ua ub]; rewrite !aux. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)