proposition: Theorem min_l : ∀ n m, n ≤ m → qeq (min n m) n.
proof: Proof. intros n m H. destruct m as [m| ]; [ idtac | destruct n; reflexivity ]. destruct n as [n| ]; [ simpl | inversion H ]. rewrite Qmin_l; [ reflexivity | inversion H; assumption ]. Qed.
imports: Utf8 QArith Misc