IntegralDomain_isLeReal (p.jasmin.2025.06.1.doc.jasmin.jasmin.Jasmin.Ssrnum.Num.IntegralDomain

type 'r axioms_ = {

coq_Rle : 'r Ssrbool.rel;
coq_Rlt : 'r Ssrbool.rel;
norm : 'r -> 'r;

}

val coq_Rle : 
  'a1 Ssralg.GRing.Coq_isNmodule.axioms_ ->
  'a1 Choice.Coq_hasChoice.axioms_ ->
  'a1 Eqtype.Coq_hasDecEq.axioms_ ->
  'a1 Ssralg.GRing.Nmodule_isSemiRing.axioms_ ->
  'a1 Ssralg.GRing.SemiRing_hasCommutativeMul.axioms_ ->
  'a1 Ssralg.GRing.Nmodule_isZmodule.axioms_ ->
  'a1 Ssralg.GRing.Ring_hasMulInverse.axioms_ ->
  'a1 Ssralg.GRing.ComUnitRing_isIntegral.axioms_ ->
  'a1 axioms_ ->
  'a1 Ssrbool.rel

val coq_Rlt : 
  'a1 Ssralg.GRing.Coq_isNmodule.axioms_ ->
  'a1 Choice.Coq_hasChoice.axioms_ ->
  'a1 Eqtype.Coq_hasDecEq.axioms_ ->
  'a1 Ssralg.GRing.Nmodule_isSemiRing.axioms_ ->
  'a1 Ssralg.GRing.SemiRing_hasCommutativeMul.axioms_ ->
  'a1 Ssralg.GRing.Nmodule_isZmodule.axioms_ ->
  'a1 Ssralg.GRing.Ring_hasMulInverse.axioms_ ->
  'a1 Ssralg.GRing.ComUnitRing_isIntegral.axioms_ ->
  'a1 axioms_ ->
  'a1 Ssrbool.rel

val norm : 
  'a1 Ssralg.GRing.Coq_isNmodule.axioms_ ->
  'a1 Choice.Coq_hasChoice.axioms_ ->
  'a1 Eqtype.Coq_hasDecEq.axioms_ ->
  'a1 Ssralg.GRing.Nmodule_isSemiRing.axioms_ ->
  'a1 Ssralg.GRing.SemiRing_hasCommutativeMul.axioms_ ->
  'a1 Ssralg.GRing.Nmodule_isZmodule.axioms_ ->
  'a1 Ssralg.GRing.Ring_hasMulInverse.axioms_ ->
  'a1 Ssralg.GRing.ComUnitRing_isIntegral.axioms_ ->
  'a1 axioms_ ->
  'a1 ->
  'a1

val phant_Build : 
  'a1 Ssralg.GRing.Coq_isNmodule.axioms_ ->
  'a1 Choice.Coq_hasChoice.axioms_ ->
  'a1 Eqtype.Coq_hasDecEq.axioms_ ->
  'a1 Ssralg.GRing.Nmodule_isSemiRing.axioms_ ->
  'a1 Ssralg.GRing.SemiRing_hasCommutativeMul.axioms_ ->
  'a1 Ssralg.GRing.Nmodule_isZmodule.axioms_ ->
  'a1 Ssralg.GRing.Ring_hasMulInverse.axioms_ ->
  'a1 Ssralg.GRing.ComUnitRing_isIntegral.axioms_ ->
  Ssralg.GRing.IntegralDomain.coq_type ->
  'a2 Ssralg.GRing.IntegralDomain.axioms_ ->
  'a2 Ssralg.GRing.Coq_isNmodule.axioms_ ->
  'a2 Choice.Coq_hasChoice.axioms_ ->
  'a2 Eqtype.Coq_hasDecEq.axioms_ ->
  'a2 Ssralg.GRing.Nmodule_isSemiRing.axioms_ ->
  'a2 Ssralg.GRing.SemiRing_hasCommutativeMul.axioms_ ->
  'a2 Ssralg.GRing.Nmodule_isZmodule.axioms_ ->
  'a2 Ssralg.GRing.Ring_hasMulInverse.axioms_ ->
  'a2 Ssralg.GRing.ComUnitRing_isIntegral.axioms_ ->
  'a1 Ssrbool.rel ->
  'a1 Ssrbool.rel ->
  ('a1 -> 'a1) ->
  'a1 axioms_

type ('r, 'rlocal) phant_axioms = 'r axioms_