proposition: Lemma erecdef_unique1 c f (m := slength c): echelon c -> slistpl f m -> (forall i, i <c m -> let a:= P (Vg c i) in let b := Q (Vg c i) in [/\ a = \0c -> Vg f i = h1 b, b = \0c -> Vg f i = h2 (Vl f a) & a <> \0c -> b <> \0c -> Vg f i = h3 (Vl f a) (Vl f b)]) -> f = echelon_recdef c.
proof: Proof. move => ha hc hd. have he:= (erecdef_prop ha). apply: erecdef_unique => // i lim. rewrite / erecdef_combine; move:(hd _ lim). set a := P _; set b := Q _; move => [ka kb kc]. case: (p_or_not_p (a = \0c)) => az; Ytac0; first by apply: (ka az). case: (p_or_not_p (b = \0c)) => bz; Ytac0; first by apply: (kb bz). by apply: kc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)