proposition: Lemma fine_expand r : (`|r| < 1)%R -> (fine (expand r))%:E = expand r.
proof: Proof. by move=> r1; rewrite /expand 2!leNgt ltrNl; case/ltr_normlP : r1 => -> ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed