proposition: Lemma plus_comm: forall x y, x + y == y + x.
proof: Proof. Proof comm QnonNeg.plus QnonNeg.plus_comm. Lemma mult_comm: forall x y, x * y == y * x. Proof comm QnonNeg.mult QnonNeg.mult_comm. Lemma plus_assoc: forall x y z, x + (y + z) == (x + y) + z. Proof assoc QnonNeg.plus QnonNeg.plus_assoc. Lemma mult_assoc: forall x y z, x * (y * z) == (x * y) * z. Proof assoc QnonNeg.mult QnonNeg.mult_assoc. Global Instance: Proper (eq ==> eq ==> eq) plus. Proof liftM2_Proper _. Global Instance: Proper (eq ==> eq ==> eq) mult. Proof liftM2_Proper _. Definition le (x y: T): Prop := match y with | Infinite => True | Finite y' => match x with | Infinite => False | Finite x' => (proj1_sig x' <= proj1_sig y') end end. Global Instance: Proper (eq ==> eq ==> iff) le. Proof with intuition. unfold eq, QnonNeg.eq, le. repeat intro. destruct x0, y0, y, x... rewrite <- H. rewrite <- H0... rewrite H. rewrite H0... Qed.
imports: CoRN.model.structures.QposInf