proposition: Lemma frac_part_mult a b : frac_part a = 0 -> frac_part b = 0 -> frac_part (a * b) = 0.
proof: Proof. rewrite /frac_part /Int_part !minus_IZR //. move=> Ha Hb. have {}Ha : IZR (up a) = a + 1. move: Ha. set x := IZR (up a). move=> Ha. rewrite -[X in X = _](add0R _) -Ha. by field. have {}Hb : IZR (up b) = b + 1. move: Hb. set x := IZR (up b). move=> Hb. rewrite -[X in X = _](add0R _) -Hb. by field. rewrite -(tech_up _ ((up a - 1) * (up b - 1) + 1)). rewrite ?plus_IZR ?minus_IZR ?mult_IZR ?minus_IZR // Ha Hb. by field. rewrite ?plus_IZR ?minus_IZR ?mult_IZR ?minus_IZR // Ha Hb. rewrite (_ : forall a, a + 1 - 1 = a); last by move=> *; field. rewrite (_ : forall a, a + 1 - 1 = a); last by move=> *; field. Lra.lra. rewrite ?plus_IZR ?minus_IZR ?mult_IZR ?minus_IZR // Ha Hb. rewrite (_ : forall a, a + 1 - 1 = a); last by move=> *; field. rewrite (_ : forall a, a + 1 - 1 = a); last by move=> *; field. by apply/RleP; rewrite Order.POrderTheory.lexx. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)