proposition: Lemma funny_compare_lemma: forall x y, clos_trans_1n (nat+nat) (lift_rel_union TA TB SA SB) x y -> funny_compare x y.
proof: Proof. intros. induction H. destruct x; destruct y; unfold funny_compare in *; simpl in *. unfold TA in *; lia. unfold SA in *; lia. unfold SB in *; lia. unfold TB in *; lia. destruct x; destruct y; destruct z; unfold funny_compare in *; simpl in *. unfold TA in *; lia. unfold TA in *; lia. unfold SA in *; lia. unfold SA in *; lia. unfold SB in *; lia. unfold SB in *; lia. unfold TB in *; lia. unfold TB in *; lia. Defined.
imports: Coq(Relations Lia) AlmostFull.PropBounded(AlmostFull) AlmostFull.PropBounded(AlmostFullInduction) AlmostFull.PropBounded(AFConstructions)