proposition: Lemma succ_pred_induction y (P : Z → Prop) : P y → (∀ x, y ≤ x → P x → P (Z.succ x)) → (∀ x, x ≤ y → P x → P (Z.pred x)) → (∀ x, P x).
proof: Proof. intros H0 HS HP. by apply (Z.order_induction' _ _ y). Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)