proposition: Lemma ltcr_pmul (x1 y1 x2 y2 : creal F) : (0 < x1)%CR -> (0 < y2)%CR -> (x1 < y1)%CR -> (x2 < y2)%CR -> (x1 * x2 < y1 * y2)%CR.
proof: Proof. move=> px1 px2 lt1 lt2. have aux : (x1 * x2 < x1 * y2)%CR by apply: ltcr_mul2l. by apply: lt_creal_trans aux _; apply: ltcr_mul2r. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals)