proposition: Lemma adjacent_to_irreflexive : Irreflexive adjacent_to.
proof: Proof. unfold Irreflexive; unfold Reflexive; unfold complement. intros x H_x. inversion H_x. auto. Qed.
imports: Verdi(Verdi) StructTact(Fin) Coq(OrderedType) Coq(MSetInterface)