proposition: Lemma minus_le : forall a b, a <= b -> a - b = zero.
proof: Proof. destruct 1. subst b; apply minus_a_a. apply minus_lt;auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List