proposition: Lemma ltrNger : forall x y, (x <<! y) = ~~ (y <<= x).
proof: Proof. Proof . by move=> x y; rewrite lerNgtr negbK . Qed . Lemma lerTl : forall x y, x <<= y -> forall z, x+z <<= y+z . Proof . by case G => T [? []] . Qed . Lemma lerTr : forall x y, x <<= y -> forall z, z+x <<= z+y . Proof . by move=> x y Hxy z; rewrite ![z+_]addrC; apply lerTl . Qed . Lemma lerTlb : forall z x y, (x+z <<= y+z) = (x <<= y) . Proof . move=> z x y; apply /idP/idP => H; last by apply lerTl . rewrite -[x](addr0) -(addrN z) -[y](addr0) -(addrN z) . by rewrite !addrA; apply lerTl . Qed . Lemma lerTrb : forall z x y, (z+x <<= z+y) = (x <<= y) . Proof . by move=> z x y; rewrite ![z+_]addrC; apply lerTlb . Qed . Lemma ltrTl : forall x y, x <<! y -> forall z, x+z <<! y+z . Proof . move=> x y H z; rewrite ltr_lerne; apply/andP; split . + by apply lerTl; apply ltrW . + rewrite ltr_lerne in H; case/andP: H => _ H . by apply/eqP => Hz; rewrite (addIr Hz) eqxx in H . Qed . Lemma ltrTr : forall x y, x <<! y -> forall z, z+x <<! z+y . Proof . by move=> x y Hxy z; rewrite ![z+_]addrC; apply ltrTl . Qed . Lemma ltrTlb : forall z x y, (x+z <<! y+z) = (x <<! y) . Proof . move=> z x y; apply/idP/idP => H; last by apply ltrTl . rewrite -[x](addr0) -(addrN z) -[y](addr0) -(addrN z) . by rewrite !addrA; apply ltrTl . Qed . Lemma ltrTrb : forall z x y, (z+x <<! z+y) = (x <<! y) . Proof . by move=> z x y; rewrite ![z+_]addrC; apply ltrTlb . Qed . Lemma lerT : forall (x₁ y₁ x₂ y₂ : G), x₁ <<= y₁ -> x₂ <<= y₂ -> x₁ + x₂ <<= y₁ + y₂ . Proof . move=> x₁ y₁ x₂ y₂ Hx Hy; apply ler_trans with (x₁+y₂) . by apply lerTr . by apply lerTl . Qed . Lemma lerT0 : forall (x y : G), 0 <<= x -> 0 <<= y -> 0 <<= x + y . Proof . by move=> x y Hx Hy; rewrite -[0]addr0; apply lerT . Qed . Lemma ler0T : forall (x y : G), x <<= 0 -> y <<= 0 -> x + y <<= 0. Proof . by move=> x y Hx Hy; rewrite -[0]add0r; apply lerT . Qed . Lemma ltrT : forall (x₁ y₁ x₂ y₂ : G), x₁ <<! y₁ -> x₂ <<! y₂ -> x₁ + x₂ <<! y₁ + y₂ . Proof . move=> x₁ y₁ x₂ y₂ H1 H2; apply ltr_ler_trans with (y₁ + x₂) . - by apply ltrTl . - by apply: lerT; rewrite ?ler_refl //; apply: ltrW. Qed . Lemma ltr_lerT : forall (x₁ y₁ x₂ y₂ : G), x₁ <<! y₁ -> x₂ <<= y₂ -> x₁ + x₂ <<! y₁ + y₂ . Proof . move=> x₁ y₁ x₂ y₂ H1 H2; apply ltr_ler_trans with (y₁ + x₂) . by apply ltrTl . by apply lerTr . Qed . Lemma ltrT0 : forall (x y : G), 0 <<! x -> 0 <<! y -> 0 <<! x + y . Proof . move=> x y Hx Hy; rewrite -[0]addr0; apply ltrT => //. Qed . Lemma ltr0T : forall (x y : G), x <<! 0 -> y <<! 0 -> x + y <<! 0. Proof . by move=> x y Hx Hy; rewrite -[0]add0r; apply ltrT . Qed . Lemma ler_oppger : forall x y, (-x <<= -y) = (y <<= x) . Proof . move=> x y; rewrite -(lerTlb x) addNr -(lerTrb y) . by rewrite addrA addrN addr0 add0r . Qed . Lemma le0r_geNr0 : forall x, (0 <<= -x) = (x <<= 0) . Proof . by move => x; rewrite -{1}oppr0 ler_oppger . Qed . Lemma ger0_leNr0 : forall x, (0 <<= x) = (- x <<= 0). Proof. by move=> x; rewrite -{2}oppr0 ler_oppger. Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)