proposition: Lemma minus_a_a : forall a, a - a = zero.
proof: Proof. induction a;simpl;auto. case a1. case (le_lt_dec n n). auto. intros; absurd (n < n)%nat; auto with arith. case (lt_eq_lt_dec n n ). destruct s. absurd (n < n)%nat;auto with arith. intros;rewrite compare_rw2. rewrite IHa2;auto. intro; absurd (n<n)%nat;auto with arith. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List