proposition: Lemma Qle_trans : forall x y z, x<=y -> y<=z -> x<=z.
proof: Proof. unfold Qle; intros (x1, x2) (y1, y2) (z1, z2); simpl; intros. Open Scope Z_scope. apply Z.mul_le_mono_pos_r with (Zpos y2); [easy|]. apply Z.le_trans with (y1 * Zpos x2 * Zpos z2). - rewrite Z.mul_shuffle0. now apply Z.mul_le_mono_pos_r. - rewrite Z.mul_shuffle0, (Z.mul_shuffle0 z1). now apply Z.mul_le_mono_pos_r. Close Scope Z_scope. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool