fact: Record ordering_pair (A:Type) (eq:A -> A -> Prop) (lt le : A -> A -> Prop) := mk_ordering_pair { lt_morph: forall x x', eq x x' -> forall y y', eq y y' -> (lt x y <-> lt x' y'); lt_irrefl : forall x, ~ lt x x; lt_antisym : forall x y, lt x y -> ~lt y x; lt_trans : forall x y z, lt x y -> lt y z -> lt x z; le_morph : forall x x', eq x x' -> forall y y', eq y y' -> (le x y <-> le x' y'); le_refl : forall x, le x x; le_antisym : forall x y, le x y -> le y x -> eq x y; le_trans : forall x y z, le x y -> le y z -> le x z; le_lt_compat_left : forall x y z, le x y -> lt y z -> lt x z; le_lt_compat_right : forall x y z, lt x y -> le y z -> lt x z; lt_included_le : forall x y, lt x y -> le x y }.
imports: Coq(List ZArith Lia) CoLoR(weaved_relation equational_theory term_spec terminaison)