proposition: Lemma cantor_tri_order_gltP x x': glt cantor_tri_order x x' <-> [/\ inc x cantor_tri_sub, inc x' cantor_tri_sub & exists j, [/\ natp j, (forall i, natp i -> i <c j -> Vg x i = Vg x' i), Vg x j = C0 & Vg x' j = C1]].
proof: Proof. rewrite /cantor_tri_order. set r := Nat_order;set g := cantor_tri_aux. have op: orprod_ax r g by apply: cantor_tri_order_axioms. have sr: substrate r = Nat by rewrite /r (proj2 Nat_order_wor). have rvP: forall j, natp j -> forall u v, (glt (Vg g j) (Vg u j) (Vg v j) <-> (Vg u j = C0 /\ Vg v j = C1)). move=> j jN u v; rewrite /g/cantor_tri_aux LgV// /glt; split. by move => [] /cdo_gleP h1; case: h1 => // [][-> ->]. move=> [ -> -> ]; split; [ apply /cdo_gleP; in_TP4 | fprops]. have rijP: forall i j, natp j -> (glt r i j <-> (natp i /\ i <c j)). move => i j jN; split;first by move => [] /Nat_order_leP [pa pb pc] pd. by move => [pa [pb pc]]; split => //; apply/Nat_order_leP. split. move => [] /(orprod_gleP op); rewrite cantor_tri_order_sr1. move=> [p1 p2 p3] p4; split => //; case: p3; first by move=> aux. rewrite sr;move=> [j [jsr /(rvP _ jsr) [pa pb] lt2]]. by exists j; split => // i iN ij; apply: lt2; apply / rijP. move=> [p1 p2 [j [jb jp1 jp2 jp3]]]; split. apply /(orprod_gleP op);rewrite cantor_tri_order_sr1;split => //. right;exists j;split => //;[ ue | by apply/rvP | ]. move => i /(rijP _ _ jb) [pa pb]; apply: (jp1 _ pa pb). move=> uv; rewrite uv jp3 in jp2; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)