proposition: Theorem min_or : forall n m : nat, min n m = n /\ n <= m \/ min n m = m /\ m < n.
proof: Proof. intros n; elim n; simpl in |- *; auto with arith. intros n' Rec m; case m; simpl in |- *; auto with arith. intros m'; elim (Rec m'); intros H'0; case H'0; clear H'0; intros H'0 H'1; rewrite H'0; auto with arith. Qed.
imports: Reals ZArith List PeanoNat Psatz