proposition: Lemma ribbon_on_conn4 b1 b2 : connect neig4 b1 b2.
proof: Proof. apply: (connect_trans _ (ribbon_on_conn4_box_ex b2)). by rewrite conn4_sym ribbon_on_conn4_box_ex. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition