proposition: Lemma one_sum : forall (x y : N), x + y = 1 -> (x = 1 /\ y = 0) |_| (x = 0 /\ y = 1).
proof: 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.
imports: HoTT.Basics.Decidable HoTT.Classes.interfaces.orders HoTT.Classes.implementations.peano_naturals HoTT.Classes.theory.rings HoTT.Classes.isomorphisms.rings HoTT.Classes.interfaces.naturals