n m : n = 0 /\ m = 0 <~> n + m = 0. Proof. srapply equiv_iff_hprop. - intros [-> ->]; reflexivity. - destruct n. + by split. + intros H; symmetry in H. by apply neq_nat_zero_succ in H. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids