proposition: Lemma Exercise2_7A9: closure (Lf (fun z => Yo (evenp z) z (csucc z)) Nat Nat) Nat_order.
proof: Proof. move: Nat_order_wor Exercise2_7A7 => [[ob _] sb] ta. split => //. split => //; first by saw => //; apply: lf_function. move=> x y /Nat_order_leP [xB yB xy]; rewrite !LfV//. apply /Nat_order_leP;split => //; try apply:ta => //. Ytac evx; Ytac evy => //. exact: (cleT xy (cleS yB)). apply /(cleSltP xB); split =>// q; apply: evx; ue. by apply /(cleSSP (CS_nat xB) (CS_nat yB)). move=> x; rewrite sb => xN; move:(NS_succ xN) =>sxN. rewrite LfV//; apply /(Nat_order_leP); split => //; Ytac evx; fprops. move=>x ;rewrite sb => xN; rewrite (LfV ta xN);move: (NS_succ xN) => sxN. by Ytac evx; rewrite LfV//; [ | move: (succ_of_odd (conj xN evx)) => ok ]; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)