proposition: Lemma frac_part_pow a : frac_part a = 0 -> forall n : nat, frac_part (a ^ n) = 0.
proof: Proof. move=> Ha; elim=> /=. by rewrite /frac_part (_ : 1 = INR 1) // Int_part_INR subRR. move=> n IH; exact: frac_part_mult. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)