proposition: Lemma onem_eq0 r : (`1-r = 0) <-> (r = 1).
proof: Proof. by rewrite /onem; split => [/subr0_eq//|->]; rewrite subrr. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(lra ring Rstruct)