proposition: Lemma Exercise2_7A11 x w (u :=Lf (fun z => Yo (evenp z) (csucc z) z) Nat Nat) (v :=Lf (fun z => Yo (evenp z) z (csucc z)) Nat Nat): natp x -> (Vf u x) <=c w -> (Vf v x) <=c w -> x <> w.
proof: Proof. move=> xB le1 le2 xw; rewrite /u/v. suff: (csucc x) <=c w by apply /(cleSltP xB); case. move: (Exercise2_7A7)(Exercise2_7A8) => p1 p2. by move: le1 le2;rewrite /u/v !LfV//; Ytac evx; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)