proposition: Lemma nat_to_B_ifle a b u v: let N := nat_to_B in N (if a <= b then u else v) = Yo (N a <=c N b)(N u)(N v).
proof: Proof. simpl;case: (ltnP b a); last by move/nat_to_B_le => ea; Ytac0. by move/nat_to_B_lt /cltNge => ea; rewrite (Y_false ea). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)