proposition: Lemma semi_ring: semi_ring_theory (R:=T) 0%Qnn 1%Qnn plus mult eq.
proof: Proof. constructor. apply plus_0_l. apply plus_comm. apply plus_assoc. apply mult_1_l. apply mult_0_l. apply mult_comm. apply mult_assoc. apply mult_plus_distr. Qed.
imports: Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program