proposition: Lemma sub_acyclic : {homo acyclic : g g' / subrel g g' >-> g' -> g}.
proof: Proof. move=> g g' subg /acyclicP[gxx /(sub_preacyclic _) pag]. apply/acyclicP; split; last by apply: pag => x y /subg/connect1. by move=> x; apply: contra (gxx x); apply: subg. Qed.
imports: mathcomp(all_ssreflect) extra