proposition: Lemma inclusion_step2_ct A (r r' r'': relation A) : r ⊆ r'' -> r' ⊆ r'' -> r ⨾ r' ⊆ r''⁺.
proof: Proof. ins; rewrite H, H0, <- ct_ct; eauto with hahn. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets