proposition: Lemma lerr x : x <= x.
proof: Proof. have n2: `|2| == 2 :> R by rewrite -ge0_def ltW ?addr_gt0 ?lt01. rewrite le_def subrr -(inj_eq (addrI `|0|)) addr0 -mulr2n -mulr_natr. by rewrite -(eqP n2) -normM mul0r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)