proposition: Lemma subgraph_empty n m : ~~ g n m -> subgraph m n == set0.
proof: Proof. move=> nm; apply/eqP/setP => i; by rewrite /subgraph /= (negbTE nm). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext