proposition: Lemma nat_1_plus_ne_0 x : 1 + x <> 0.
proof: Proof. intro E. destruct (zero_sum 1 x E). apply nat_nontrivial. trivial. 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