proposition: Lemma mult_1_l: forall x, 1%Qnn * x == x.
proof: Proof. Proof binop_unit_left Qmult 1 Qle_0_1 Qmult_le_0_compat Qmult_le_compat Qmult_1_l. Lemma mult_comm: forall x y, x * y == y * x. Proof binop_comm Qmult Qmult_le_0_compat Qmult_comm. Lemma mult_assoc: forall n m p, n * (m * p) == (n * m) * p. Proof binop_assoc Qmult Qmult_le_0_compat Qmult_comm Qmult_assoc Qmult_le_compat. Lemma mult_plus_distr n m p: (n + m) * p == n * p + m * p. Proof with auto; simpl. unfold eq. split. intros _ [_ _ [e d ?? b ?][g f ?? c ?]a ?] r ? ... apply BinopBound_le with (e * d + g * f)%Qnn... apply Qle_trans with (`b + `c)%Q... apply Qplus_le_compat... apply Qle_trans with (`a)... apply is_binop_bound with (e + g)%Qnn (QnonNeg.min d f)... apply is_binop_bound with e g... apply QnonNeg.min_case... apply (is_bound_Proper p)... rewrite Qmult_plus_distr_l. apply Qplus_le_compat... do 2 rewrite (Qmult_comm (`e)). apply Qmult_le_compat_r... apply Q.le_min_l. do 2 rewrite (Qmult_comm (`g)). apply Qmult_le_compat_r... apply Q.le_min_r. intros q [a b [c d ?? e ?] ? r1 ?] r E... apply BinopBound_le with ((c + d) * b)%Qnn... apply Qle_trans with (`e * `b)%Q... apply Qmult_le_compat_r... apply Qle_trans with (`r1)... apply is_binop_bound with (c * b)%Qnn (d * b)%Qnn. apply is_binop_bound with c b... apply is_binop_bound with d b... simpl. ring_simplify... Qed.
imports: Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program