proposition: Lemma diag_pow_decomp_mod k X T: forall x y, k > 1 -> clos_trans_1n _ (@lift_diag k X T) x y -> clos_trans_1n X (power k T) (snd x) (snd y) /\ eq_fin (fst x) (fst y) \/ ~ (eq_fin (fst x) (fst y)).
proof: Proof. intros x y kGt CT. destruct (diag_pow_decomp kGt CT) as (m,H). destruct H. destruct H0. destruct H1. destruct H1. subst m. left. split. apply H2. destruct x. destruct y. unfold fst in *. unfold snd in *. simpl. unfold plus_mod in H0. destruct f. destruct f0. unfold eq_fin in *. simpl in H0. auto. right. destruct H1. destruct x. destruct y. unfold plus_mod in H0. unfold fst in *. unfold snd in *. destruct f. destruct f0. unfold eq_fin in *. subst x2. apply plus_mod_diff. firstorder. firstorder. firstorder. apply H. Defined.
imports: Coq(Arith Relations Lia) AlmostFull.PropBounded(AlmostFull) AlmostFull.PropBounded(AFConstructions)