proposition: Lemma ltrP : forall x y, ltr_xor_ger x y (x <<! y) (y <<= x) .
proof: Proof. Proof . move=> x y; rewrite lerNgtr; case Hxy: (x <<! y); constructor=> // . by rewrite lerNgtr Hxy . Qed . CoInductive compare x y : bool -> bool -> bool -> Set := | CompareLt of x <<! y : compare x y true false false | CompareGt of y <<! x : compare x y false true false | CompareEq of x = y : compare x y false false true . Lemma compareP : forall x y, compare x y (x <<! y) (y <<! x) (x == y) . Proof . move=> x y; rewrite ltrNger eq_ler andbC ltr_lerne . case: ltrP; [by constructor | rewrite ler_ltreq; case: lerP => //=] . + by move=> _; move/eqP => ->; rewrite eqxx; constructor . + by move=> Hxy _; rewrite (ltr_ne Hxy); constructor . Qed . Lemma ltrNgtr : forall x y, x <<! y -> ~~(y <<! x) . Proof . by move=> x y; case: compareP . Qed . Lemma χ0_ltr : forall n, (0 : G) <<! 1 *+ (n.+1). have HnSn : forall n, (n%:R : G) <<! n.+1%:R . + by elim=> [|n IH]; [apply ltr_0_1 | rewrite 2!mulrS; apply ltrTr] . elim=> [|n IH]; [by apply ltr_0_1 | apply: ltr_trans] . by apply IH . by rewrite 2!mulrS; apply ltrTr; apply HnSn . Qed . Lemma χ0 : forall n, 1 *+ n.+1 != 0 :> G. Proof . move=> n; case D: (n.+1%:R == 0) => //= . by move/eqP: D => D; have H := χ0_ltr n; rewrite D ltr_irrefl in H . Qed . Lemma sign_posR : forall x, 0 <<! x -> sign x = 1 . Proof . by move=> x hx; rewrite /sign hx. Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)