proposition: Lemma cantor_tri_order_sr : substrate cantor_tri_order = cantor_tri_sub.
proof: Proof. rewrite /cantor_tri_order orprod_sr. apply: cantor_tri_order_sr1. apply: cantor_tri_order_axioms. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)