proposition: Lemma af_power_induction_non_trivial: forall (A:Type) k (T : A -> A -> Prop) (R : A -> A -> Prop), k > 1 -> almost_full R -> (forall x y, @clos_trans_1n _ (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 X k T R kGt afR Hct P frec. assert (forall (x: Finite k * X), P (snd x)). apply af_induction with (T := @lift_diag k X T) (R := @lift_pointwise k X R). unfold lift_pointwise; apply af_intersection. apply af_cofmap; apply af_finite. apply af_cofmap; apply afR. intros x y (CTxy,Tyx). induction CTxy. unfold lift_diag in H. unfold lift_pointwise in Tyx. unfold next_fin in H. destruct x. destruct y. simpl in H. destruct f. destruct f0. simpl in Tyx. destruct H. unfold eq_fin in H. unfold eq_fin in Tyx. lia. destruct x as ((kx,Hx),x). destruct y as ((ky,Hy),y). destruct z as ((kz,Hz),z). unfold lift_diag in H. unfold next_fin in H. simpl in H. destruct H as (H2,H4). unfold lift_pointwise in Tyx. simpl in Tyx. unfold eq_fin in Tyx. destruct Tyx as (H3,H5). assert (clos_trans_1n X (power k T) x z /\ kx = kz \/ (kx <> kz)). assert (@clos_trans_1n (Finite k * X) (@lift_diag k X T) (FinIntro (k:=k) (x:=kx) Hx, x) (FinIntro (k:=k) (x:=kz) Hz, z)). constructor 2 with (y := (@FinIntro k ky Hy,y)). unfold lift_diag. unfold fst. unfold snd. split. unfold next_fin. apply H2. apply H4. apply CTxy. destruct (diag_pow_decomp_mod kGt H). simpl in H0. destruct H0. left. split. apply H0. unfold eq_fin in H1. apply H1. unfold eq_fin in H0. unfold fst in H0. right. apply H0. firstorder. intros. destruct x as ((kx,Hx),x). unfold snd. apply frec. intros. destruct kx. assert (k-1 < k). lia. intros. apply (X0 (@FinIntro k (k-1) H0,y)). simpl. unfold lift_diag. unfold fst. unfold snd. split. unfold next_fin. lia. apply H. assert (kx < k). intuition auto; lia. intros. apply (X0 (@FinIntro k kx H0,y)). simpl. unfold lift_diag. simpl. split. simpl. unfold next_fin. right. intuition lia. apply H. intros. apply frec. intros. apply (X0 (@FinIntro k 1 kGt, y)). Defined.
imports: Coq(Arith Relations Lia) AlmostFull.PropBounded(AlmostFull) AlmostFull.PropBounded(AFConstructions)