proposition: Lemma af_power_induction: forall (A:Type) k (T : A -> A -> Prop) (R : A -> A -> Prop), k >= 1 -> almost_full R -> (forall x y, clos_trans_1n A (power k T) x y /\ R y x -> False) -> forall P : A -> Type, (forall x, (forall y, T y x -> P y) -> P x) -> forall x, P x.
proof: Proof. intros. destruct (le_lt_dec k 1). assert (k = 1). lia. apply af_induction with (T := T) (R := R). apply H0. intros. eapply H1. split. 2: { destruct H3. apply r. } subst k. simpl. destruct H3. clear H3 H H1 l. induction H2. constructor. exists y. auto. constructor 2 with (y := y). exists y. auto. auto. apply X. apply af_power_induction_non_trivial with (k := k) (T := T) (R := R). lia. assumption. assumption. assumption. Defined.
imports: Coq(Arith Relations Lia) AlmostFull.PropBounded(AlmostFull) AlmostFull.PropBounded(AFConstructions)