proposition: Theorem min_dec : ∀ n m, {min n m = n} + {min n m = m}.
proof: Proof. intros n m. destruct n as [n| ]; [ idtac | destruct m; right; reflexivity ]. destruct m as [m| ]; [ idtac | left; reflexivity ]. destruct (Qmin_dec n m) as [H| H]; simpl; rewrite H. left; reflexivity. right; reflexivity. Qed.
imports: Utf8 QArith Misc