proposition: Lemma acyclic_mon A (r r' : relation A) : acyclic r -> r' ⊆ r -> acyclic r'.
proof: Proof. eby repeat red; ins; eapply H, clos_trans_mon. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets