proposition: Lemma ribbon_on_conn4_skew : conn4_skew inner outer.
proof: Proof. rewrite /conn4_skew; apply/eqP/esym. rewrite -(n_comp_connect conn4_sym boxex). by apply: eq_n_comp_r => b; rewrite !inE ribbon_on_conn4_box_ex. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition