proposition: Lemma seq_minus_transitive A (r r1 r2 : relation A) (TR : transitive r) : r1 ⨾ r2 \ r ⊆ (r1 \ r) ⨾ r2 ∪ (r1 ∩ r) ⨾ (r2 \ r).
proof: Proof. autounfold with unfolderDb; ins; desf. destruct (classic (r x z)); [|eauto]. right; eexists; splits; try edone; intro; eauto. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets