proposition: Theorem induction_ltof1 : forall P:A -> Type, (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a.
proof: Proof. intros P F. assert (H : forall n (a:A), f a < n -> P a). { intro n; induction n as [|n IHn]. - intros a Ha; absurd (f a < 0); auto. apply Nat.nlt_0_r. - intros a Ha. apply F. unfold ltof. intros b Hb. apply IHn. apply Nat.lt_le_trans with (f a); auto. now apply Nat.succ_le_mono. } intros a. apply (H (S (f a))). apply Nat.lt_succ_diag_r. Defined.
imports: PeanoNat