proposition: Lemma restrict_irrefl (T : Type) (e : rel T) (A : pred T) : irreflexive e -> irreflexive (restrict A e).
proof: Proof. move => irr_e x /=. by rewrite irr_e. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)