proposition: Lemma cantor_tri_order_total : total_order cantor_tri_order.
proof: Proof. rewrite /cantor_tri_order/cantor_tri_aux; apply: orprod_total. by apply: cantor_tri_order_axioms. red; aw => i iN; rewrite !LgV//; apply: (worder_total (proj1 cdo_wor)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)