proposition: Lemma diag_pow_decomp k X T: forall x y, k > 1 -> clos_trans_1n _ (@lift_diag k X T) x y -> exists m, m < k /\ (eq_fin (fst y) (@plus_mod k m (fst x))) /\ ((m = O /\ clos_trans_1n _ (power k T) (snd x) (snd y)) \/ ((m > 0 /\ exists z: Finite k * X, power m T (snd x) (snd z) /\ clos_refl_trans _ (power k T) (snd z) (snd y)))).
proof: Proof. intros x y kGt. intro CT. induction CT. unfold lift_diag in H. unfold next_fin in H. simpl in H. destruct x as ((kx,Hx),x). destruct y as ((ky,Hy),y). simpl in H. exists 1. split. firstorder. split. destruct H. destruct H. destruct H. subst k. unfold plus_mod. unfold fst. unfold eq_fin. auto. unfold plus_mod_aux. simpl. rewrite Nat.sub_diag. apply H1. unfold plus_mod. unfold fst. unfold eq_fin. auto. unfold plus_mod_aux. remember (k - S kx) as diff. destruct diff. lia. lia. right. split. lia. exists (@FinIntro k ky Hy, y). split. simpl. exists y. firstorder. simpl. apply rt_refl. destruct IHCT as (m,(MltK,(HEqfin,G))). destruct G. destruct H0. subst m. destruct x as ((kx,Hx),x). destruct y as ((ky,Hy),y). destruct z as ((kz,Hz),z). unfold fst in *. unfold snd in *. unfold lift_diag in H. unfold fst in *. unfold snd in *. simpl in H. unfold next_fin in H. destruct H. unfold plus_mod in HEqfin. unfold eq_fin in HEqfin. exists (S O). split. lia. split. unfold plus_mod. unfold eq_fin. destruct H. destruct H. subst ky. simpl in HEqfin. subst kz. simpl. remember (k - S kx) as diff. destruct diff. auto. lia. simpl. destruct H. subst ky. simpl in HEqfin. subst kz. remember (k - S kx) as diff. destruct diff. lia. reflexivity. right. split. auto. exists (@FinIntro k ky Hy,y). split. simpl. exists y. split. apply H0. reflexivity. apply ctr_from_ct. apply H1. destruct H0. destruct H1. destruct H1. destruct (eq_nat_dec k (S m)). exists O. split. lia. split. 2: { left. assert (power k T (snd x) (snd x0)). subst k. simpl. exists (snd y). split. destruct H. apply H3. apply H1. split. reflexivity. eapply ct_from_ctr. 2: apply H2. constructor 1. subst k. simpl. exists (snd y). split. destruct H. apply H4. apply H1. } destruct x as ((kx,Hx),x). destruct y as ((ky,Hy),y). destruct z as ((kz,Hz),z). unfold fst. unfold plus_mod. simpl. unfold eq_fin. unfold fst in HEqfin. unfold plus_mod in HEqfin. unfold eq_fin in HEqfin. subst kz. subst k. unfold lift_diag in H. unfold fst in H. unfold snd in H. unfold next_fin in H. simpl in H. destruct H. destruct H. destruct H. subst ky. inversion H. assert (plus_mod_aux (S m) m O = (m + O)%nat). apply plus_mod_lt. lia. rewrite H4. auto. destruct H. subst ky. apply plus_mod_suc. lia. exists (S m). split. lia. split. 2: { right. split. lia. exists x0. split. simpl. exists (snd y). split. destruct H. apply H3. apply H1. apply H2. } destruct x as ((kx,Hx),x). destruct y as ((ky,Hy),y). destruct z as ((kz,Hz),z). unfold fst. unfold plus_mod. unfold eq_fin. unfold plus_mod in HEqfin. unfold fst in *. unfold snd in *. unfold eq_fin in HEqfin. subst kz. unfold lift_diag in H. unfold fst in H. unfold snd in H. destruct H. unfold next_fin in H. destruct H. destruct H. subst. simpl. rewrite Nat.sub_diag. reflexivity. simpl. destruct H. subst ky. remember (k - S kx) as diff. destruct diff. lia. reflexivity. Defined.
imports: Coq(Arith Relations Lia) AlmostFull.PropBounded(AlmostFull) AlmostFull.PropBounded(AFConstructions)