proposition: Lemma le01 : 0 <= 1.
proof: Proof. have n1_nz: `|1| != 0 :> R by apply: contraNneq (@oner_neq0 R) => /norm_eq0->. by rewrite ge0_def -(inj_eq (mulfI n1_nz)) -normM !mulr1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)