proposition: Lemma Exercise2_7A10: closure (Lf (fun z => Yo (evenp z) (csucc z) z) Nat Nat) Nat_order.
proof: Proof. move: Nat_order_wor Exercise2_7A8 => [[ob _] sb] ta. split => //. split => //; first by red;aw; split =>//; apply: lf_function. move=> x y /Nat_order_leP [xN yN xy]; rewrite !LfV//; apply /Nat_order_leP. move: (NS_succ xN)(NS_succ yN) => sxN syN. split => //;fprops; Ytac evx => //;Ytac evy => //. by apply /(cleSSP (CS_nat xN) (CS_nat yN)). apply /(cleSltP xN); split =>// q; apply: evy; ue. exact: (cleT xy (cleS yN)). move=> x;rewrite sb => xN; move: (NS_succ xN) => sxN. apply /Nat_order_leP; rewrite LfV//;split => //; Ytac evx; fprops. move=>x ;rewrite sb => xN; move: (NS_succ xN) => sxN. rewrite (LfV ta xN); Ytac evx; rewrite LfV//; fprops;last by Ytac0. by rewrite (Y_false (proj2(succ_of_even evx))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)