proposition: Lemma sqrf_eq1 x : (x ^+ 2 == 1) = (x == 1) || (x == -1).
proof: Proof. by rewrite -subr_eq0 subr_sqr_1 mulf_eq0 subr_eq0 addr_eq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)