proposition: Lemma binop_unit_left (x: T): binop u_nn x == x.
proof: Proof. Proof with auto. unfold eq, le. simpl. split. intros. apply (is_binop_bound) with u_nn q... simpl. rewrite o_u_left... intros q [q0 q' H1 H2 v H3] r vr. apply closed_le with q'... apply Qle_trans with (`v)... rewrite <- (o_u_left (`q')). apply Qle_trans with (o (`q0) (`q'))... Qed.
imports: Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program