proposition: Lemma axioms_of_order r: order r <-> (order_axioms r (substrate r)).
proof: Proof. rewrite/order_axioms; split. move => [p1 p2 p3 p4]. split => //. by move => x y xy; split; order_tac. by move => x; split => h; try order_tac; apply: p2. move=> [h1 h2 h3 h4 gr]; split => //; by move => y /h4. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)