proposition: Lemma Qpos_min_mult_distr_l : forall x y z : Qpos, QposEq (Qpos_mult (Qpos_min y z) x) (Qpos_min (Qpos_mult y x) (Qpos_mult z x)).
proof: Proof. intros x y z. unfold QposEq. rewrite Q_Qpos_min. simpl. rewrite Q_Qpos_min. apply Qmin_mult_pos_distr_l. apply Qlt_le_weak. destruct x. exact q. Qed.
imports: Coq.Logic.Eqdep_dec Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qpower Coq.QArith.Qround CoRN.model.totalorder.QMinMax CoRN.order.TotalOrder