proposition: Lemma powE A (r : relation A) n a b : (r ^^ n) a b <-> exists f, f 0 = a /\ f n = b /\ forall i, i < n -> r (f i) (f (S i)).
proof: Proof. split. generalize b; induction n; ins; unfold seq, eqv_rel in *; desf. exists (fun x => b0); splits; ins; lia. specialize (IHn _ H); desf. exists (fun x => if eq_op x (S n) then b0 else f x); ins; desf; desf. splits; ins; desf; ins; desf; try lia; eauto. apply IHn1; lia. ins; desf; induction n; ins; exists (f n); split; eauto. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets