proposition: Lemma nat_to_B_ifeq a b u v: let N := nat_to_B in N (if a == b then u else v) = Yo (N a = N b)(N u)(N v).
proof: Proof. case: ifP => ab; first by rewrite(eqP ab) /=(Y_true (erefl _)). by rewrite /= Y_false // =>/nat_to_B_injective xab; move: ab; rewrite xab eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)