proposition: Lemma connect_iter (A : ob fhrel_monoid_ops) (e : fhrel_monoid_ops A A) (x y : A): connect e x y <-> (exists u : nat, rel.iter A e u x y).
proof: Proof. split. - case/connectP => p pth_p lst_p. exists (size p). elim: p x pth_p lst_p => /= [x _ -> // | z p IHp x /andP [xz pth_p] lst_p]. exists z => //. exact: IHp. - case => n. elim: n x => /= [x <- // |n IHn x [z xz H]]. exact: connect_trans (connect1 xz) (IHn _ _). Qed.
imports: Setoid Morphisms kat normalisation rewriting kat_tac comparisons rel relalg boolean mathcomp(all_ssreflect)