proposition: Lemma square_pos (a: R): a != 0 -> 0 < a * a.
proof: Proof. by move => anz; rewrite lt0r sqr_ge0 sqrf_eq0 anz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polydiv polyorder path interval polyrcf)