proposition: Lemma sign_codomP : forall x, [\/ sign x = 1, sign x = -1 | sign x = 0] .
proof: Proof. Proof . move=> x; case: (compareP 0 x) => H; [apply Or31 | apply Or32 | apply Or33] . - by apply: sign_posR. - by apply: sign_negR. - by rewrite -H sign0 . Qed . Lemma absr_nneg : forall x, 0 <<= x -> absr x = x . Proof . move=> x Hx; rewrite /absr ltrNger . by case D: (0 <<= x) => //=; rewrite Hx in D . Qed . Lemma absr_npos : forall x, x <<= 0 -> absr x = -x . Proof . move=> x Hx; rewrite /absr ltrNger; case Hx': (0 <<= x) => //= . have Hx0: x = 0 by apply/eqP; rewrite eq_ler Hx Hx' . by rewrite Hx0 oppr0 . Qed . Lemma absr_neg : forall x, x <<! 0 -> absr x = -x . Proof . by move=> x Hx; apply absr_npos; apply ltrW . Qed . Lemma absr0 : absr 0 = 0 :> G . Proof . by rewrite /absr ltr_irrefl . Qed . Lemma absrpos : forall x, 0 <<= absr x . Proof . move=> x; case: (ltrP x 0) => H . + by rewrite absr_neg // le0r_geNr0; apply ltrW . + by rewrite absr_nneg. Qed . Lemma absrK : forall x, absr (absr x) = absr x . Proof . by move=> x; rewrite absr_nneg // absrpos . Qed . Lemma absr_oppr : forall x, absr(-x) = absr x. Proof. move=> x. case a : (0 <<! x). by rewrite (absr_nneg (ltrW a)) absr_npos ?opprK // -oppr0 ler_oppger ltrW. move: (negbT a); rewrite -lerNgtr => a'; rewrite (absr_npos a'). by rewrite absr_nneg // -ler_oppger opprK oppr0. Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)