proposition: Lemma ler0_addl_abs : forall x y, 0 <<= x -> (absr y) <<= x -> 0 <<= x + y .
proof: Proof. Proof . by move=> x y Hx Hy; apply ler_addl_abs; last rewrite oppr0 addr0 . Qed . End OComringTheory . Module OField . Record class_of (R : Type) : Type := Class { base1 :> GRing.Field.class_of R; ext :> OComRing.mixin_of (GRing.Field.Pack base1 R) } . Coercion base2 R m := @OComRing.Class R _ (@ext R m). Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}. Definition class cT := let: Pack _ c _ := cT return class_of cT in c. Definition unpack K (k : forall T (c : class_of T), K T c) cT := let: Pack T c _ := cT return K _ (class cT) in k _ c. Definition repack cT : _ -> Type -> type := let k T c p := p c in unpack k cT. Definition pack := let k T c m := Pack (@Class T c m) T in GRing.Field.unpack k. Definition eqType cT := Equality.Pack (class cT) cT. Definition choiceType cT := Choice.Pack (class cT) cT. Definition zmodType cT := GRing.Zmodule.Pack (class cT) cT. Definition ringType cT := GRing.Ring.Pack (class cT) cT. Definition unitRingType cT := GRing.UnitRing.Pack (class cT) cT. Definition comRingType cT := GRing.ComRing.Pack (class cT) cT. Definition comUnitRingType cT := GRing.ComUnitRing.Pack (class cT) cT. Definition idomainType cT := GRing.IntegralDomain.Pack (class cT) cT. Coercion fieldType cT := GRing.Field.Pack (class cT) cT. Coercion oComRingType cT := OComRing.Pack (class cT) cT. Definition oFieldType cT := @OComRing.Pack (fieldType cT) (class cT) cT. End OField . Canonical Structure OField.eqType. Canonical Structure OField.choiceType. Canonical Structure OField.zmodType. Canonical Structure OField.ringType. Canonical Structure OField.comRingType. Canonical Structure OField.unitRingType. Canonical Structure OField.comUnitRingType. Canonical Structure OField.idomainType. Canonical Structure OField.fieldType. Canonical Structure OField.oComRingType. Bind Scope ring_scope with OField.sort. Section OrderedFieldTheory. Variable G : OField.type . Implicit Types x y : G. Lemma ltr_0_lcompat : forall x y, 0 <<! x -> 0 <<! y -> 0 <<! x * y . Proof . move=> x y Hx Hy; rewrite ltr_lerne; apply/andP; split . + by apply ler_0_lcompat; apply ltrW . + rewrite eq_sym mulf_eq0 negb_or . by rewrite ![_ == 0]eq_sym (ltr_ne Hx) (ltr_ne Hy) . Qed . Lemma oppreq_0 : forall x, (x == -x) = (x == 0) . Proof . move=> x; apply/eqP/eqP => [|->]; last by rewrite oppr0 . move/(congr1 (+%R x)); rewrite addrN -{1 2}[x](mul1r) -mulr_addl . move/eqP; rewrite mulf_eq0; case/orP; last by move/eqP => -> . by rewrite (negbTE (χ0 G 1%nat)). Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)