proposition: Theorem ominus_def : forall m n : nat, match ominus m n with | Some q => m = n + q | None => m < n end.
proof: Proof. intros m; elim m; simpl in |- *; auto with arith. intros n; case n; simpl in |- *; auto with arith. intros m1 Rec n; case n; simpl in |- *; auto with arith. intros n1; generalize (Rec n1); case (ominus m1 n1); simpl in |- *; auto with arith. Qed.
imports: Coq(Arith ArithRing)