proposition: Lemma ler_0_lcompat : forall x y, 0 <<= x -> 0 <<= y -> 0 <<= x * y .
proof: Proof. Proof . by move=> x y Hx Hy; rewrite -[0](mulr0 x); apply ler_lcompat . Qed . Lemma ler_neg0_lcompat : forall x y, x <<= 0 -> y <<= 0 -> 0 <<= x * y . Proof . move=> x y Hx Hy . by rewrite -mulrNN; apply ler_0_lcompat; rewrite le0r_geNr0 . Qed . Lemma ltr_0_1 : 0 <<! (1 : G) . Proof . rewrite ltr_lerne /negb eq_sym oner_eq0 andbT . case/orP: (ler_total 0 1) => // H . by rewrite -[1](mulr1 1); apply ler_neg0_lcompat . Qed . Lemma ler_add_0l : forall x y, 0 <<= x -> 0 <<= y -> x+y = 0 -> x = 0 . Proof . move=> x y Hx Hy; move/(congr1 (+%R^~ -y)) . rewrite -addrA addrN addr0 add0r; move=> H; subst x . rewrite -ler_oppger oppr0 in Hy . by apply/eqP; rewrite eq_ler Hx Hy . Qed . Lemma ler_add_0r : forall x y, 0 <<= x -> 0 <<= y -> x+y = 0 -> y = 0 . Proof . move=> x y Hx Hy Hxy; apply ler_add_0l with x => // . by rewrite addrC . Qed . CoInductive ler_xor_gtr (x y : G) : bool -> bool -> Set := | LerNotGtr of x <<= y : ler_xor_gtr x y true false | GtrNotLer of y <<! x : ler_xor_gtr x y false true . CoInductive ltr_xor_ger (x y : G) : bool -> bool -> Set := | LtrNotGer of x <<! y : ltr_xor_ger x y true false | GerNotLtr of y <<= x : ltr_xor_ger x y false true . Lemma lerP : forall x y, ler_xor_gtr x y (x <<= y) (y <<! x) . Proof. move=> x y; rewrite ltrNger; case Hxy: (x <<= y); constructor=> // . by rewrite ltrNger Hxy . Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)