proposition: Lemma mult_0_l (x: T): 0%Qnn * x == 0%Qnn.
proof: Proof. Proof with auto. split... unfold le. simpl. intros. apply (is_binop_bound) with 0%Qnn (bound x)... simpl. rewrite Qmult_0_l... Qed.
imports: Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program