proposition: Lemma bsteps_ind_r (P : nat → A → Prop) (x : A) (Prefl : ∀ n, P n x) (Pstep : ∀ n y z, bsteps R n x y → R y z → P n y → P (S n) z) : ∀ n z, bsteps R n x z → P n z.
proof: Proof. cut (∀ m y z, bsteps R m y z → ∀ n, bsteps R n x y → (∀ m', n ≤ m' ∧ m' ≤ n + m → P m' y) → P (n + m) z). { intros help n. change n with (0 + n). eauto. } induction 1 as [|m x' y z p2 p3 IH]; [by eauto with arith|]. intros n p1 H. rewrite <-plus_n_Sm. apply (IH (S n)); [by eauto using bsteps_r |]. intros [|m'] [??]; [lia |]. apply Pstep with x'. - apply bsteps_weaken with n; intuition lia. - done. - apply H; intuition lia. Qed.
imports: stdpp(options)