proposition: Lemma neig4_sym rc1 rc2 : rc1 \in neig4 rc2 -> rc2 \in neig4 rc1.
proof: Proof. rewrite /neig4 /=; case: rc1 rc2 => [r1 c1][r2 c2]; rewrite !inE. move/or4P => [] /eqP[-> ->]; rewrite /= ?eqxx ?orbT //=. - by case: c2 => [|c2]; rewrite /= ?eqxx ?orbT. - by case: r2 => [|r2]; rewrite /= ?eqxx ?orbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition