proposition: Lemma sign_pos : forall x, reflect (sign x = 1) (0 <<! x) .
proof: Proof. Proof . move=> x; rewrite /sign; case: (compareP 0 x) => h; constructor => //. + by apply/eqP; rewrite eq_sym oppreq_0 nonzero1r. + by apply/eqP; rewrite eq_sym nonzero1r. Qed . Lemma sign_neg : forall x, reflect (sign x = -1) (x <<! 0) . Proof . move=> x; rewrite /sign; case: (compareP 0 x) => _; constructor=> // . + apply/eqP; rewrite oppreq_0; exact: nonzero1r . + move/(congr1 -%R); rewrite opprK oppr0; move/eqP . by rewrite eq_sym (negbTE (nonzero1r _)) . Qed . Lemma mulr_sign : forall x y, sign (x * y) = (sign x) * (sign y) . Proof . move=> x y; case: (compareP 0 x) . + case: (compareP 0 y) => Hy Hx . * by rewrite !sign_posR ?mul1r //; apply ltr_0_lcompat . * rewrite [sign x]sign_posR // !sign_negR ?mul1r // . rewrite -lt0r_gtNr0 -mulrN; apply ltr_0_lcompat => // . by rewrite lt0r_gtNr0 . * by rewrite -Hy mulr0 sign0 mulr0 . + case: (compareP 0 y) => Hy Hx . * rewrite [sign y]sign_posR // !sign_negR ?mulr1 // . rewrite -lt0r_gtNr0 -mulNr; apply ltr_0_lcompat => // . by rewrite lt0r_gtNr0 . * rewrite [sign x]sign_negR // [sign y]sign_negR // . rewrite sign_posR; first by rewrite ?mulrNN ?mulr1 . by rewrite -mulrNN; apply ltr_0_lcompat; rewrite lt0r_gtNr0 . * by rewrite -Hy mulr0 sign0 mulr0 . + by move=> <-; rewrite mul0r sign0 mul0r . Qed . Lemma invr_ltr : forall x, (0 <<! x^-1) = (0 <<! x) . Proof . have Hsign : forall x, x != 0 -> sign (x^-1 * x) = 1 . + by move=> x Hx; rewrite mulVf // sign_posR // ltr_0_1 . have HP: forall x, 0 <<! x -> 0 <<! x^-1 . + move=> x Hx; apply/sign_pos; rewrite -(Hsign x) . * rewrite mulr_sign -{1}[sign x^-1]mulr1 . by congr (_ * _); symmetry; apply/sign_pos . * by rewrite eq_sym; apply (ltr_ne Hx) . move=> x; apply/idP/idP; last exact: HP . by move=> Hx; rewrite -(invrK x); apply HP . Qed . Lemma ler_Ilcompat_r : forall x y₁ y₂, 0 <<! x -> x * y₁ <<= x * y₂ -> y₁ <<= y₂ . Proof . move=> x y₁ y₂ Hx Hy . rewrite -[y₁](mul1r) -[y₂](mul1r) -[1](@mulVf _ x) 1?eq_sym ?(ltr_ne Hx) //. by rewrite -!mulrA; apply ler_lcompat => //; apply ltrW; rewrite invr_ltr . Qed . Lemma ler_Ilcompat_l : forall x y₁ y₂, 0 <<! x -> y₁ * x <<= y₂ * x -> y₁ <<= y₂ . Proof . move=> x y₁ y₂; rewrite mulrC [y₂ * _]mulrC; exact: ler_Ilcompat_r. Qed . Lemma ltr_Ilcompat_r : forall x y₁ y₂, 0 <<! x -> x * y₁ <<! x * y₂ -> y₁ <<! y₂ . Proof . move=> x y₁ y₂ Hx Hy . rewrite -[y₁](mul1r) -[y₂](mul1r) -[1](@mulVf _ x) 1?eq_sym ?(ltr_ne Hx) //. by rewrite -!mulrA; apply ltr_lcompat => //; rewrite invr_ltr . Qed . Lemma ltr_Ilcompat_l : forall x y₁ y₂, 0 <<! x -> y₁ * x <<! y₂ * x -> y₁ <<! y₂ . Proof . move=> x y₁ y₂; rewrite mulrC [y₂ * _]mulrC; exact: ltr_Ilcompat_r. Qed . Lemma invr1_ltr0_ltr1 : forall x, 0 <<! x -> (x <<! 1) = (1 <<! x^-1). Proof. move=> x hx; move:(hx); rewrite ltr_lerne eq_sym; case/andP=> hx1 hx2. rewrite -{1}(divff hx2) -{1}(mulr1 x); case e: (1 <<! x^-1). by rewrite ltr_lcompat. by rewrite ltrNger ler_lcompat // lerNgtr e. Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)