proposition: Remark strip_commut : commut A R1 R2 -> forall x y:A, clos_trans A R1 y x -> forall z:A, R2 z y -> exists2 y' : A, R2 y' x & clos_trans A R1 z y'.
proof: Proof. induction 2 as [x y| x y z H0 IH1 H1 IH2]; intros. - elim H with y x z; auto with sets; intros x0 H2 H3. exists x0; auto with sets. - elim IH1 with z0; auto with sets; intros. elim IH2 with x0; auto with sets; intros. exists x1; auto with sets. apply t_trans with x0; auto with sets. Qed.
imports: Relation_Operators Relation_Definitions Transitive_Closure