proposition: Lemma plus_eq_one_imp_eq_zero : forall m n : nat, m + n <= 1 -> {m = 0} + {n = 0}.
proof: Proof. intros m n H. elim (le_lt_dec m 0); intro. left; auto with arith. right; lia. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)