Merge pull request #123 from coq-community/coq_18590

Adapt to coq/coq#18590

.github/workflows/docker-action.yml

@@ -18,14 +18,8 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.19'
           - 'coqorg/coq:8.18'
-          - 'coqorg/coq:8.17'
-          - 'coqorg/coq:8.16'
-          - 'coqorg/coq:8.15'
-          - 'coqorg/coq:8.14'
-          - 'coqorg/coq:8.13'
-          - 'coqorg/coq:8.12'
-          - 'coqorg/coq:8.11'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3

README.md

@@ -10,8 +10,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [![Zulip][zulip-shield]][zulip-link]
 [![DOI][doi-shield]][doi-link]
 
-[docker-action-shield]: https://github.com/coq-community/math-classes/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/coq-community/math-classes/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/coq-community/math-classes/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/math-classes/actions/workflows/docker-action.yml
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
@@ -50,7 +50,7 @@ notations.
 - Coq-community maintainer(s):
   - Bas Spitters ([**@spitters**](https://github.com/spitters))
 - License: [MIT License](LICENSE)
-- Compatible Coq versions: Coq 8.11 or later (use releases for other Coq versions)
+- Compatible Coq versions: Coq 8.18 or later (use releases for other Coq versions)
 - Additional dependencies:
   - [BigNums](https://github.com/coq/bignums)
 - Coq namespace: `MathClasses`

coq-math-classes.opam

@@ -30,7 +30,7 @@ build: [
 ]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.11" & < "8.19~") | (= "dev")}
+  "coq" {(>= "8.18" & < "8.20~") | (= "dev")}
   "coq-bignums" 
 ]
 

implementations/fast_rationals.v

@@ -1,8 +1,9 @@
 Require
+  MathClasses.theory.rings
   MathClasses.theory.shiftl MathClasses.theory.int_pow.
 Require Import
   Coq.QArith.QArith Bignums.BigQ.BigQ
-  MathClasses.interfaces.abstract_algebra
+  MathClasses.interfaces.orders MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals
   MathClasses.interfaces.integers MathClasses.interfaces.rationals MathClasses.interfaces.additional_operations
   MathClasses.implementations.fast_naturals MathClasses.implementations.fast_integers MathClasses.implementations.field_of_fractions MathClasses.implementations.stdlib_rationals.
 Require Export

interfaces/abstract_algebra.v

@@ -6,9 +6,9 @@ For various structures we omit declaration of substructures. For example, if we
 say:
 
 Class Setoid_Morphism :=
-  { setoidmor_a :> Setoid A
-  ; setoidmor_b :> Setoid B
-  ; sm_proper :> Proper ((=) ==> (=)) f }.
+  { setoidmor_a :: Setoid A
+  ; setoidmor_b :: Setoid B
+  ; sm_proper :: Proper ((=) ==> (=)) f }.
 
 then each time a Setoid instance is required, Coq will try to prove that a
 Setoid_Morphism exists. This obviously results in an enormous blow-up of the
@@ -20,14 +20,14 @@ Setoid_Morphism as a substructure, setoid rewriting will become horribly slow.
 *)
 
 (* An unbundled variant of the former CoRN RSetoid *)
-Class Setoid A {Ae : Equiv A} : Prop := setoid_eq :> Equivalence (@equiv A Ae).
+Class Setoid A {Ae : Equiv A} : Prop := setoid_eq :: Equivalence (@equiv A Ae).
 
 (* An unbundled variant of the former CoRN CSetoid. We do not 
   include a proof that A is a Setoid because it can be derived. *)
 Class StrongSetoid A {Ae : Equiv A} `{Aap : Apart A} : Prop :=
-  { strong_setoid_irreflexive :> Irreflexive (≶) 
-  ; strong_setoid_symmetric :> Symmetric (≶) 
-  ; strong_setoid_cotrans :> CoTransitive (≶) 
+  { strong_setoid_irreflexive :: Irreflexive (≶)
+  ; strong_setoid_symmetric :: Symmetric (≶)
+  ; strong_setoid_cotrans :: CoTransitive (≶)
   ; tight_apart : ∀ x y, ¬x ≶ y ↔ x = y }.
 
 Arguments tight_apart {A Ae Aap StrongSetoid} _ _.
@@ -38,7 +38,7 @@ Section setoid_morphisms.
   Class Setoid_Morphism :=
     { setoidmor_a : Setoid A
     ; setoidmor_b : Setoid B
-    ; sm_proper :> Proper ((=) ==> (=)) f }. 
+    ; sm_proper :: Proper ((=) ==> (=)) f }.
 
   Class StrongSetoid_Morphism :=
     { strong_setoidmor_a : StrongSetoid A
@@ -70,80 +70,80 @@ Section upper_classes.
   Context A {Ae : Equiv A}.
 
   Class SemiGroup {Aop: SgOp A} : Prop :=
-    { sg_setoid :> Setoid A
-    ; sg_ass :> Associative (&)
-    ; sg_op_proper :> Proper ((=) ==> (=) ==> (=)) (&) }.
+    { sg_setoid :: Setoid A
+    ; sg_ass :: Associative (&)
+    ; sg_op_proper :: Proper ((=) ==> (=) ==> (=)) (&) }.
 
   Class CommutativeSemiGroup {Aop : SgOp A} : Prop :=
-    { comsg_setoid :> @SemiGroup Aop
-    ; comsg_ass :> Commutative (&) }.
+    { comsg_setoid :: @SemiGroup Aop
+    ; comsg_ass :: Commutative (&) }.
 
   Class SemiLattice {Aop : SgOp A} : Prop :=
-    { semilattice_sg :> @CommutativeSemiGroup Aop
-    ; semilattice_idempotent :> BinaryIdempotent (&)}.
+    { semilattice_sg :: @CommutativeSemiGroup Aop
+    ; semilattice_idempotent :: BinaryIdempotent (&)}.
 
   Class Monoid {Aop : SgOp A} {Aunit : MonUnit A} : Prop :=
-    { monoid_semigroup :> SemiGroup
-    ; monoid_left_id :> LeftIdentity (&) mon_unit
-    ; monoid_right_id :> RightIdentity (&) mon_unit }.
+    { monoid_semigroup :: SemiGroup
+    ; monoid_left_id :: LeftIdentity (&) mon_unit
+    ; monoid_right_id :: RightIdentity (&) mon_unit }.
 
   Class CommutativeMonoid {Aop Aunit} : Prop :=
-    { commonoid_mon :> @Monoid Aop Aunit
-    ; commonoid_commutative :> Commutative (&) }.
+    { commonoid_mon :: @Monoid Aop Aunit
+    ; commonoid_commutative :: Commutative (&) }.
 
   Class Group {Aop Aunit} {Anegate : Negate A} : Prop :=
-    { group_monoid :> @Monoid Aop Aunit
-    ; negate_proper :> Setoid_Morphism (-)
-    ; negate_l :> LeftInverse (&) (-) mon_unit
-    ; negate_r :> RightInverse (&) (-) mon_unit }.
+    { group_monoid :: @Monoid Aop Aunit
+    ; negate_proper :: Setoid_Morphism (-)
+    ; negate_l :: LeftInverse (&) (-) mon_unit
+    ; negate_r :: RightInverse (&) (-) mon_unit }.
 
   Class BoundedSemiLattice {Aop Aunit} : Prop :=
-    { bounded_semilattice_mon :> @CommutativeMonoid Aop Aunit
-    ; bounded_semilattice_idempotent :> BinaryIdempotent (&)}.
+    { bounded_semilattice_mon :: @CommutativeMonoid Aop Aunit
+    ; bounded_semilattice_idempotent :: BinaryIdempotent (&)}.
 
   Class AbGroup {Aop Aunit Anegate} : Prop :=
-    { abgroup_group :> @Group Aop Aunit Anegate
-    ; abgroup_commutative :> Commutative (&) }.
+    { abgroup_group :: @Group Aop Aunit Anegate
+    ; abgroup_commutative :: Commutative (&) }.
 
   Context {Aplus : Plus A} {Amult : Mult A} {Azero : Zero A} {Aone : One A}.
 
   Class SemiRing : Prop :=
-    { semiplus_monoid :> @CommutativeMonoid plus_is_sg_op zero_is_mon_unit
-    ; semimult_monoid :> @CommutativeMonoid mult_is_sg_op one_is_mon_unit
-    ; semiring_distr :> LeftDistribute (.*.) (+)
-    ; semiring_left_absorb :> LeftAbsorb (.*.) 0 }.
+    { semiplus_monoid :: @CommutativeMonoid plus_is_sg_op zero_is_mon_unit
+    ; semimult_monoid :: @CommutativeMonoid mult_is_sg_op one_is_mon_unit
+    ; semiring_distr :: LeftDistribute (.*.) (+)
+    ; semiring_left_absorb :: LeftAbsorb (.*.) 0 }.
 
   Context {Anegate : Negate A}.
 
   Class Ring : Prop :=
-    { ring_group :> @AbGroup plus_is_sg_op zero_is_mon_unit _
-    ; ring_monoid :> @CommutativeMonoid mult_is_sg_op one_is_mon_unit
-    ; ring_dist :> LeftDistribute (.*.) (+) }.
+    { ring_group :: @AbGroup plus_is_sg_op zero_is_mon_unit _
+    ; ring_monoid :: @CommutativeMonoid mult_is_sg_op one_is_mon_unit
+    ; ring_dist :: LeftDistribute (.*.) (+) }.
 
   (* For now, we follow CoRN/ring_theory's example in having Ring and SemiRing
     require commutative multiplication. *)
 
   Class IntegralDomain : Prop :=
     { intdom_ring : Ring 
     ; intdom_nontrivial : PropHolds (1 ≠ 0)
-    ; intdom_nozeroes :> NoZeroDivisors A }.
+    ; intdom_nozeroes :: NoZeroDivisors A }.
 
   (* We do not include strong extensionality for (-) and (/) because it can de derived *)
   Class Field {Aap: Apart A} {Arecip: Recip A} : Prop :=
-    { field_ring :> Ring
-    ; field_strongsetoid :> StrongSetoid A
-    ; field_plus_ext :> StrongSetoid_BinaryMorphism (+)
-    ; field_mult_ext :> StrongSetoid_BinaryMorphism (.*.)
+    { field_ring :: Ring
+    ; field_strongsetoid :: StrongSetoid A
+    ; field_plus_ext :: StrongSetoid_BinaryMorphism (+)
+    ; field_mult_ext :: StrongSetoid_BinaryMorphism (.*.)
     ; field_nontrivial : PropHolds (1 ≶ 0)
-    ; recip_proper :> Setoid_Morphism (//)
+    ; recip_proper :: Setoid_Morphism (//)
     ; recip_inverse : ∀ x, `x // x = 1 }.
 
   (* We let /0 = 0 so properties as Injective (/), f (/x) = / (f x), / /x = x, /x * /y = /(x * y) 
     hold without any additional assumptions *)
   Class DecField {Adec_recip : DecRecip A} : Prop :=
-    { decfield_ring :> Ring
+    { decfield_ring :: Ring
     ; decfield_nontrivial : PropHolds (1 ≠ 0)
-    ; dec_recip_proper :> Setoid_Morphism (/)
+    ; dec_recip_proper :: Setoid_Morphism (/)
     ; dec_recip_0 : /0 = 0
     ; dec_recip_inverse : ∀ x, x ≠ 0 → x / x = 1 }.
 End upper_classes.
@@ -159,7 +159,7 @@ Hint Extern 5 (PropHolds (1 ≠ 0)) => eapply @decfield_nontrivial : typeclass_i
 (* 
 For a strange reason Ring instances of Integers are sometimes obtained by
 Integers -> IntegralDomain -> Ring and sometimes directly. Making this an
-instance with a low priority instead of using intdom_ring:> Ring forces Coq to
+instance with a low priority instead of using intdom_ring:: Ring forces Coq to
 take the right way 
 *)
 #[global]
@@ -174,29 +174,29 @@ Section lattice.
   Context A `{Ae: Equiv A} {Ajoin: Join A} {Ameet: Meet A} `{Abottom : Bottom A}.
 
   Class JoinSemiLattice : Prop := 
-    join_semilattice :> @SemiLattice A Ae join_is_sg_op.
+    join_semilattice :: @SemiLattice A Ae join_is_sg_op.
   Class BoundedJoinSemiLattice : Prop := 
-    bounded_join_semilattice :> @BoundedSemiLattice A Ae join_is_sg_op bottom_is_mon_unit.
+    bounded_join_semilattice :: @BoundedSemiLattice A Ae join_is_sg_op bottom_is_mon_unit.
   Class MeetSemiLattice : Prop := 
-    meet_semilattice :> @SemiLattice A Ae meet_is_sg_op.
+    meet_semilattice :: @SemiLattice A Ae meet_is_sg_op.
 
   Class Lattice : Prop := 
-    { lattice_join :> JoinSemiLattice
-    ; lattice_meet :> MeetSemiLattice
-    ; join_meet_absorption :> Absorption (⊔) (⊓) 
-    ; meet_join_absorption :> Absorption (⊓) (⊔)}.
+    { lattice_join :: JoinSemiLattice
+    ; lattice_meet :: MeetSemiLattice
+    ; join_meet_absorption :: Absorption (⊔) (⊓) 
+    ; meet_join_absorption :: Absorption (⊓) (⊔)}.
 
   Class DistributiveLattice : Prop := 
-    { distr_lattice_lattice :> Lattice
-    ; join_meet_distr_l :> LeftDistribute (⊔) (⊓) }.
+    { distr_lattice_lattice :: Lattice
+    ; join_meet_distr_l :: LeftDistribute (⊔) (⊓) }.
 End lattice.
 
 Class Category O `{!Arrows O} `{∀ x y: O, Equiv (x ⟶ y)} `{!CatId O} `{!CatComp O}: Prop :=
-  { arrow_equiv :> ∀ x y, Setoid (x ⟶ y)
-  ; comp_proper :> ∀ x y z, Proper ((=) ==> (=) ==> (=)) (comp x y z)
-  ; comp_assoc :> ArrowsAssociative O
-  ; id_l :> ∀ x y, LeftIdentity (comp x y y) cat_id
-  ; id_r :> ∀ x y, RightIdentity (comp x x y) cat_id }.
+  { arrow_equiv :: ∀ x y, Setoid (x ⟶ y)
+  ; comp_proper :: ∀ x y z, Proper ((=) ==> (=) ==> (=)) (comp x y z)
+  ; comp_assoc :: ArrowsAssociative O
+  ; id_l :: ∀ x y, LeftIdentity (comp x y y) cat_id
+  ; id_r :: ∀ x y, RightIdentity (comp x x y) cat_id }.
       (* note: no equality on objects. *)
 
 (* todo: use my comp everywhere *)
@@ -208,46 +208,46 @@ Section morphism_classes.
   Class SemiGroup_Morphism {Aop Bop} (f : A → B) :=
     { sgmor_a : @SemiGroup A Ae Aop
     ; sgmor_b : @SemiGroup B Be Bop
-    ; sgmor_setmor :> Setoid_Morphism f
+    ; sgmor_setmor :: Setoid_Morphism f
     ; preserves_sg_op : ∀ x y, f (x & y) = f x & f y }.
 
   Class JoinSemiLattice_Morphism {Ajoin Bjoin} (f : A → B) :=
     { join_slmor_a : @JoinSemiLattice A Ae Ajoin
     ; join_slmor_b : @JoinSemiLattice B Be Bjoin
-    ; join_slmor_sgmor :> @SemiGroup_Morphism join_is_sg_op join_is_sg_op f }.
+    ; join_slmor_sgmor :: @SemiGroup_Morphism join_is_sg_op join_is_sg_op f }.
 
   Class MeetSemiLattice_Morphism {Ameet Bmeet} (f : A → B) :=
     { meet_slmor_a : @MeetSemiLattice A Ae Ameet
     ; meet_slmor_b : @MeetSemiLattice B Be Bmeet
-    ; meet_slmor_sgmor :> @SemiGroup_Morphism meet_is_sg_op meet_is_sg_op f }.
+    ; meet_slmor_sgmor :: @SemiGroup_Morphism meet_is_sg_op meet_is_sg_op f }.
 
   Class Monoid_Morphism {Aunit Bunit Aop Bop} (f : A → B) :=
     { monmor_a : @Monoid A Ae Aop Aunit
     ; monmor_b : @Monoid B Be Bop Bunit
-    ; monmor_sgmor :> SemiGroup_Morphism f
+    ; monmor_sgmor :: SemiGroup_Morphism f
     ; preserves_mon_unit : f mon_unit = mon_unit }.
 
   Class BoundedJoinSemiLattice_Morphism {Abottom Bbottom Ajoin Bjoin} (f : A → B) :=
     { bounded_join_slmor_a : @BoundedJoinSemiLattice A Ae Ajoin Abottom
     ; bounded_join_slmor_b : @BoundedJoinSemiLattice B Be Bjoin Bbottom
-    ; bounded_join_slmor_monmor :> @Monoid_Morphism bottom_is_mon_unit bottom_is_mon_unit join_is_sg_op join_is_sg_op f }.
+    ; bounded_join_slmor_monmor :: @Monoid_Morphism bottom_is_mon_unit bottom_is_mon_unit join_is_sg_op join_is_sg_op f }.
 
   Class SemiRing_Morphism {Aplus Amult Azero Aone Bplus Bmult Bzero Bone} (f : A → B) :=
     { semiringmor_a : @SemiRing A Ae Aplus Amult Azero Aone
     ; semiringmor_b : @SemiRing B Be Bplus Bmult Bzero Bone
-    ; semiringmor_plus_mor :> @Monoid_Morphism zero_is_mon_unit zero_is_mon_unit plus_is_sg_op plus_is_sg_op f
-    ; semiringmor_mult_mor :> @Monoid_Morphism one_is_mon_unit one_is_mon_unit mult_is_sg_op mult_is_sg_op f }.
+    ; semiringmor_plus_mor :: @Monoid_Morphism zero_is_mon_unit zero_is_mon_unit plus_is_sg_op plus_is_sg_op f
+    ; semiringmor_mult_mor :: @Monoid_Morphism one_is_mon_unit one_is_mon_unit mult_is_sg_op mult_is_sg_op f }.
 
   Class Lattice_Morphism {Ajoin Ameet Bjoin Bmeet} (f : A → B) :=
     { latticemor_a : @Lattice A Ae Ajoin Ameet
     ; latticemor_b : @Lattice B Be Bjoin Bmeet
-    ; latticemor_join_mor :> JoinSemiLattice_Morphism f
-    ; latticemor_meet_mor :> MeetSemiLattice_Morphism f }.
+    ; latticemor_join_mor :: JoinSemiLattice_Morphism f
+    ; latticemor_meet_mor :: MeetSemiLattice_Morphism f }.
 
   Context {Aap : Apart A} {Bap : Apart B}.
   Class StrongSemiRing_Morphism {Aplus Amult Azero Aone Bplus Bmult Bzero Bone} (f : A → B) :=
-    { strong_semiringmor_sr_mor :> @SemiRing_Morphism Aplus Amult Azero Aone Bplus Bmult Bzero Bone f
-    ; strong_semiringmor_strong_mor :> StrongSetoid_Morphism f }.
+    { strong_semiringmor_sr_mor :: @SemiRing_Morphism Aplus Amult Azero Aone Bplus Bmult Bzero Bone f
+    ; strong_semiringmor_strong_mor :: StrongSetoid_Morphism f }.
 End morphism_classes.
 
 Section jections.
@@ -267,8 +267,8 @@ Section jections.
     ; surjective_mor : Setoid_Morphism f }.
 
   Class Bijective : Prop :=
-    { bijective_injective :> Injective
-    ; bijective_surjective :> Surjective }.
+    { bijective_injective :: Injective
+    ; bijective_surjective :: Surjective }.
 End jections.
 
 #[global]

interfaces/additional_operations.v

@@ -34,7 +34,7 @@ Instance: Params (@shiftl) 3 := {}.
 
 Class ShiftLSpec A B (sl : ShiftL A B) `{Equiv A} `{Equiv B} `{One A} `{Plus A} `{Mult A} `{Zero B} `{One B} `{Plus B} := {
   shiftl_proper : Proper ((=) ==> (=) ==> (=)) (≪) ;
-  shiftl_0 :> RightIdentity (≪) 0 ;
+  shiftl_0 :: RightIdentity (≪) 0 ;
   shiftl_S : ∀ x n, x ≪ (1 + n) = 2 * x ≪ n
 }.
 
@@ -71,7 +71,7 @@ Instance: Params (@shiftr) 3 := {}.
 
 Class ShiftRSpec A B (sl : ShiftR A B) `{Equiv A} `{Equiv B} `{One A} `{Plus A} `{Mult A} `{Zero B} `{One B} `{Plus B} := {
   shiftr_proper : Proper ((=) ==> (=) ==> (=)) (≫) ;
-  shiftr_0 :> RightIdentity (≫) 0 ;
+  shiftr_0 :: RightIdentity (≫) 0 ;
   shiftr_S : ∀ x n, x ≫ n = 2 * x ≫ (1 + n) ∨ x ≫ n = 2 * x ≫ (1 + n) + 1
 }.
 

interfaces/canonical_names.v

@@ -405,12 +405,12 @@ Notation "f ⁻¹" := (inverse f) (at level 30) : mc_scope.
 Class Idempotent `{ea : Equiv A} (f: A → A → A) (x : A) : Prop := idempotency: f x x = x.
 Arguments idempotency {A ea} _ _ {Idempotent}.
 
-Class UnaryIdempotent `{Equiv A} (f: A → A) : Prop := unary_idempotent :> Idempotent (@compose A A A) f.
+Class UnaryIdempotent `{Equiv A} (f: A → A) : Prop := unary_idempotent :: Idempotent (@compose A A A) f.
 
 Lemma unary_idempotency `{Equiv A} `{!Reflexive (=)} `{!UnaryIdempotent f} x : f (f x) = f x.
 Proof. firstorder. Qed.
 
-Class BinaryIdempotent `{Equiv A} (op: A → A → A) : Prop := binary_idempotent :> ∀ x, Idempotent op x.
+Class BinaryIdempotent `{Equiv A} (op: A → A → A) : Prop := binary_idempotent :: ∀ x, Idempotent op x.
 
 Class LeftIdentity {A} `{Equiv B} (op : A → B → B) (x : A): Prop := left_identity: ∀ y, op x y = y.
 Class RightIdentity `{Equiv A} {B} (op : A → B → A) (y : B): Prop := right_identity: ∀ x, op x y = x.
@@ -428,7 +428,7 @@ Class Commutative `{Equiv B} `(f : A → A → B) : Prop := commutativity: ∀ x
 Class HeteroAssociative {A B C AB BC} `{Equiv ABC}
      (fA_BC: A → BC → ABC) (fBC: B → C → BC) (fAB_C: AB → C → ABC) (fAB : A → B → AB): Prop
    := associativity : ∀ x y z, fA_BC x (fBC y z) = fAB_C (fAB x y) z.
-Class Associative `{Equiv A} f := simple_associativity:> HeteroAssociative f f f f.
+Class Associative `{Equiv A} f := simple_associativity:: HeteroAssociative f f f f.
 Notation ArrowsAssociative C := (∀ {w x y z: C}, HeteroAssociative (◎) (comp z _ _ ) (◎) (comp y x w)).
 
 Class Involutive `{Equiv A} (f : A → A) := involutive: ∀ x, f (f x) = x.
@@ -451,8 +451,8 @@ Class LeftHeteroDistribute {A B} `{Equiv C} (f : A → B → C) (g_r : B → B 
   := distribute_l : ∀ a b c, f a (g_r b c) = g (f a b) (f a c).
 Class RightHeteroDistribute {A B} `{Equiv C} (f : A → B → C) (g_l : A → A → A) (g : C → C → C) : Prop
   := distribute_r: ∀ a b c, f (g_l a b) c = g (f a c) (f b c).
-Class LeftDistribute`{Equiv A} (f g: A → A → A) := simple_distribute_l :> LeftHeteroDistribute f g g.
-Class RightDistribute `{Equiv A} (f g: A → A → A) := simple_distribute_r :> RightHeteroDistribute f g g.
+Class LeftDistribute`{Equiv A} (f g: A → A → A) := simple_distribute_l :: LeftHeteroDistribute f g g.
+Class RightDistribute `{Equiv A} (f g: A → A → A) := simple_distribute_r :: RightHeteroDistribute f g g.
 
 Class HeteroSymmetric {A} {T : A → A → Type} (R : ∀ {x y}, T x y → T y x → Prop) : Prop :=
   hetero_symmetric `(a : T x y) (b : T y x) : R a b → R b a.