proposition: Lemma expandN r : expand (- r)%R = - expand r.
proof: Proof. rewrite /expand; case: ifPn => [r1|]. rewrite ifF; [by rewrite ifT // -lerNr|apply/negbTE]. by rewrite -ltNge -(opprK r) -ltrNl (lt_le_trans _ r1) // -subr_gt0 opprK. rewrite -ltNge => r1; case: ifPn; rewrite lerNl opprK; [by move=> ->|]. by rewrite -ltNge leNgt => ->; rewrite leNgt -ltrNl r1 /= mulNr normrN. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed