proposition: Lemma plus_is_zero : forall a b, nf a -> nf b -> a + b = zero -> a = zero /\ b = zero.
proof: Proof. destruct a;destruct b. compute. auto. simpl. discriminate 3. intro;rewrite plus_a_zero. discriminate 2. auto. simpl. case a1;case b1. discriminate 3. intros c n1 c0 H H0; rewrite compare_rw1. discriminate 1. constructor. intros c n1 c0 H H0; rewrite compare_rw3. discriminate 1. constructor. intros c n1 c0 c3 n2 c4 H H0; case (compare (cons c3 n2 c4) (cons c n1 c0));discriminate 1. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List