proposition: Lemma absr_sign : forall x , (absr x) = (sign x) * x .
proof: Proof. Proof . move=> x; case: (compareP x 0) => h. + by rewrite /absr h; move/sign_negR: h=> ->; rewrite mulN1r. + by rewrite absr_nneg ?ltrW //; move/sign_posR: h=> ->; rewrite mul1r . + by rewrite h sign0 absr0 mul0r. Qed . Lemma absr_addr : forall x y, absr (x + y) <<= (absr x) + (absr y). move=> x y; rewrite !absr_sign. case: (compareP x 0) => hx. - rewrite (sign_negR hx) mulN1r; case: (compareP y 0) => hy. + rewrite (sign_negR hy) mulN1r mulr_addr. rewrite (_ : sign _ = -1) ?mulN1r ?ler_refl //; apply: sign_negR. by apply: ltr0T. + rewrite (sign_posR hy) mul1r ; case: (compareP (x + y) 0) => hxy. * by rewrite (sign_negR hxy) mulr_addr !mulN1r lerTrb opp_ler_ler0 ltrW. * by rewrite (sign_posR hxy) mul1r lerTlb ler_opp_ler0 ltrW. * by rewrite hxy sign0 mul0r lerT0 // ?le0r_geNr0 ltrW. + by rewrite hy mulr0 !addr0 (sign_negR hx) mulN1r ler_refl. - rewrite (sign_posR hx) mul1r; case: (compareP y 0) => hy. + rewrite (sign_negR hy) mulN1r mulr_addr; case: (compareP (x + y) 0) => hxy. * by rewrite (sign_negR hxy) !mulN1r lerTlb opp_ler_ler0 ltrW. * by rewrite (sign_posR hxy) !mul1r lerTrb ler_opp_ler0 ltrW. * by rewrite hxy sign0 !mul0r addr0 lerT0 // ?le0r_geNr0 ltrW. + rewrite (sign_posR hy) mul1r (_ : sign _ = 1) ?mul1r ?ler_refl //. by apply: sign_posR; apply: ltrT0. + by rewrite hy mulr0 !addr0 (sign_posR hx) mul1r ler_refl. - by rewrite hx mulr0 !add0r ler_refl. Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)