proposition: Lemma T2_ct_invariant: forall x y, clos_trans_1n _ (power 2 T) x y -> fst x < fst y /\ snd x < fst y \/ snd x < snd y /\ fst x < snd y \/ fst x < fst y /\ snd x < snd y.
proof: Proof. intros x y CT. induction CT. apply T2_invariant; assumption. remember (T2_invariant H) as G; clear HeqG CT H. destruct G as [G1 | [G2 | G3]]; destruct IHCT as [IH1 | [IH2 | IH3]]. left; lia. right; left; lia. left; lia. left; lia. right; left; lia. right; left; lia. left; lia. right; left; lia. right; right; lia. Defined.
imports: Coq(Relations Lia) AlmostFull.PropBounded(AlmostFull) AlmostFull.PropBounded(AlmostFullInduction) AlmostFull.PropBounded(AFConstructions)