proposition: Lemma pow_add R n m (s t : X) : pow R (n + m) s t <-> rcomp (pow R n) (pow R m) s t.
proof: Proof. revert m s t; induction n; intros m s t. - simpl. split; intros. econstructor. split. unfold pow. simpl. reflexivity. eassumption. destruct H as [u [H1 H2]]. unfold pow in H1. simpl in *. subst s. eassumption. - simpl in *; split; intros. + destruct H as [u [H1 H2]]. change (it (rcomp R) (n + m) eq) with (pow R (n+m)) in H2. rewrite IHn in H2. destruct H2 as [u' [A B]]. unfold pow in A. econstructor. split. econstructor. repeat split; repeat eassumption. eassumption. + destruct H as [u [H1 H2]]. destruct H1 as [u' [A B]]. econstructor. split. eassumption. change (it (rcomp R) (n + m) eq) with (pow R (n + m)). rewrite IHn. econstructor. split; eassumption. Qed.
imports: Undecidability.Shared.Libs.PSL.Base Lia Arith Arith