proposition: Lemma T_empty_intersect: forall x y, clos_trans_1n _ T x y -> R y x -> False.
proof: Proof. intros x y CT HR. assert (T x y \/ clos_trans_1n (nat*nat) (power 2 T) x y \/ exists z, T x z /\ clos_trans_1n _ (power 2 T) z y). 2: { destruct H. destruct H. destruct HR. lia. destruct HR. lia. destruct H. destruct (T2_ct_invariant H). destruct HR. lia. destruct HR. lia. destruct H. destruct H. destruct (T2_ct_invariant H0). firstorder; lia. firstorder; lia. } clear HR. induction CT. left; auto. destruct IHCT. right. left. constructor. exists y. auto. split. apply H. exists z. split. auto. auto. unfold power. reflexivity. destruct H0. right. right. exists y. split. apply H. apply H0. destruct H0. destruct H0. right. left. constructor 2 with (y := x0). exists y. split. apply H. exists x0. split. auto. simpl. reflexivity. apply H1. Defined.
imports: Coq(Relations Lia) AlmostFull.PropBounded(AlmostFull) AlmostFull.PropBounded(AlmostFullInduction) AlmostFull.PropBounded(AFConstructions)