LtLe_isPOrder (p.jasmin.2025.06.3.doc.jasmin.jasmin.Jasmin.Order.Order.LtLe

type 't axioms_ = {

le : 't Ssrbool.rel;
lt : 't Ssrbool.rel;

}

val le : 
  unit ->
  'a1 Eqtype.Coq_hasDecEq.axioms_ ->
  'a1 axioms_ ->
  'a1 Ssrbool.rel

val lt : 
  unit ->
  'a1 Eqtype.Coq_hasDecEq.axioms_ ->
  'a1 axioms_ ->
  'a1 Ssrbool.rel

val phant_Build : 
  unit ->
  'a1 Eqtype.Coq_hasDecEq.axioms_ ->
  Eqtype.Equality.coq_type ->
  'a2 Eqtype.Equality.axioms_ ->
  'a2 Eqtype.Coq_hasDecEq.axioms_ ->
  'a1 Ssrbool.rel ->
  'a1 Ssrbool.rel ->
  'a1 axioms_

type ('t, 'tlocal) phant_axioms = 't axioms_