proposition: Lemma transitiveI A (r: relation A) : inclusion (r ⨾ r) r <-> transitive r.
proof: Proof. red; splits; unfold transitive, inclusion, seq; ins; desf; eauto. Qed.
imports: HahnBase HahnList HahnRelationsBasic HahnEquational HahnFuneq HahnSets