proposition: Theorem minus_lt_0 : forall m n : nat, n < m -> n - m = 0.
proof: Proof. intros m; elim m; simpl in |- *; auto. intros n H; absurd (n < 0); auto with arith. intros n H' n0; case n0; simpl in |- *; auto with arith. Qed.
imports: Coq(Arith Compare Compare_dec Peano_dec) Coq(Relation_Definitions EqdepFacts Eqdep_dec)