proposition: Lemma plus_eq_zero : forall a b : nat, a + b =N= 0 -> a =N= 0 /\ b =N= 0.
proof: Proof. intros [|a];[intros [|b];auto|]. - intros E. destruct (S_neq_0 _ E). - intros ? E. destruct (S_neq_0 _ E). Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.naturals HoTT.Classes.interfaces.orders HoTT.Classes.theory.rings HoTT.Classes.orders.semirings HoTT.Classes.theory.apartness