proposition: Lemma contract_lt1 r : (`|contract r%:E| < 1)%R.
proof: Proof. rewrite normrM normrV ?unitfE //. rewrite ltr_pdivrMr // ?mul1r//; last by rewrite gtr0_norm. by rewrite [ltRHS]gtr0_norm ?ltrDr// ltr_pwDl. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed