proposition: Theorem min_comm : ∀ n m, qeq (min n m) (min m n).
proof: Proof. intros n m. destruct n as [n| ]; [ simpl | destruct m; reflexivity ]. destruct m as [m| ]; [ simpl | reflexivity ]. rewrite Qmin_comm; reflexivity. Qed.
imports: Utf8 QArith Misc