proposition: Lemma splitr x : x = x / 2%:R + x / 2%:R.
proof: Proof. by rewrite -mulr2n -mulr_natr mulfVK //= pnatr_eq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)