proposition: Lemma plus_is_zero alpha beta : nf alpha -> nf beta -> alpha + beta = zero -> alpha = zero /\ beta = zero.
proof: Proof. destruct alpha, beta. - now split. - cbn; discriminate 3. - now rewrite plus_zero_r. - case alpha1; case beta1. 1-3: discriminate. simpl. intros * Hnf_1 Hnf_2. rewrite compare_cons. destruct (compare alpha0 alpha) eqn:?. 2-3: easy. destruct (n2 ?= n1) eqn:?. 2-3: easy. now destruct (compare beta0 beta) eqn:?. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)