proposition: Lemma cantor_tri_order_axioms: orprod_ax Nat_order cantor_tri_aux.
proof: Proof. rewrite/cantor_tri_aux;move : Nat_order_wor => [pa pb]. split=> //;hnf;aw;trivial=> i ib ; rewrite !LgV//. by move: cdo_wor => [[ok _] _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)