proposition: Lemma le_0_Qpos (x: Qpos): le 0 x.
proof: Proof. destruct x. simpl. apply Qlt_le_weak, q. Qed.
imports: CoRN.model.totalorder.QposMinMax Coq.Setoids.Setoid Coq.Arith.Arith CoRN.model.rings.Qring CoRN.model.structures.QposInf CoRN.stdlib_omissions.Q MathClasses.interfaces.abstract_algebra MathClasses.implementations.stdlib_rationals MathClasses.theory.setoids