proposition: Lemma lte_sqr x y : 0 <= x -> 0 <= y -> (x ^+ 2 < y ^+ 2) = (x < y).
proof: Proof. move=> xge0 yge0; apply/idP/idP; rewrite !expe2. by apply: contra_lt => yltx; apply: lee_pmul. by move=> xley; apply: lte_pmul. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed