proposition: Lemma pow2_Rlt_inv a b : 0 <= a -> 0 <= b -> a ^ 2 < b ^ 2 -> a < b.
proof: Proof. move=> ? ? H. apply sqrt_lt_1 in H; try exact: pow_even_ge0. by rewrite /= !mulR1 !sqrt_square in H. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)