proposition: Lemma plus_resp_Npos0 : forall x y : nat, x <> 0 -> y <> 0 -> (x+y) <> 0.
proof: Proof. intros x y H H0. unfold not in |- *. intros H1. unfold not in H. apply H. lia. Qed.
imports: CoRN.model.structures.Nsec Coq(Arith Lia)