proposition: Lemma cantor_tri_order_sr1 : prod_of_substrates cantor_tri_aux = cantor_tri_sub.
proof: Proof. congr (productb);rewrite /fam_of_substrates /cantor_tri_aux; aw. apply: Lg_exten; move=> x xN /=; rewrite LgV//; exact: (proj2 cdo_wor). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)