forall (x y : N), x + y = 1 -> (x = 1 /\ y = 0) |_| (x = 0 /\ y = 1). Proof. refine (from_nat_stmt nat (fun s => forall (x y : s), x + y = 1 -> (x = 1 /\ y = 0) |_| (x = 0 /\ y = 1)) _). simpl. intros [|x] [|y];auto. - intros E. rewrite add_S_l,add_0_r in E. apply S_inj in E. rewrite E. auto. - intros E. rewrite add_S_l,add_S_r in E. apply S_inj in E. destruct (S_neq_0 _ E). Qed.
Require Import Require Import Import SemiRings.