proposition: Lemma fsum_pow2_empty: forall x y : nat + nat, clos_trans_1n (nat + nat) (power 2 Tfsum) x y /\ Rfsum y x -> False.
proof: Proof. intros. destruct H. induction H. - destruct H. destruct H. destruct H1. destruct H1. destruct H. destruct H. destruct H. subst x. subst x0. destruct y. destruct H0. destruct H1. destruct H. destruct H. inversion H. destruct H. destruct H. inversion H1. unfold Rfsum in H0. unfold sum_lift in H0. inversion H. subst. inversion H2. subst. lia. unfold Rfsum in H0. unfold sum_lift in H0. destruct H1. destruct H. destruct H. destruct H1. subst. destruct y; auto. destruct H1. subst. inversion H. subst. simpl in H2. inversion H2. subst. lia. destruct H1. destruct H1. simpl in H2. destruct y. subst. inversion H2. destruct x; auto. subst. destruct H. destruct H. inversion H. - unfold Rfsum in *. unfold sum_lift in *. clear H1. destruct z. * destruct x; auto. destruct y; subst. + inversion H. destruct H1. inversion H2. destruct H3. inversion H4. subst. clear H2 H4. inversion H3. destruct H2. destruct H2. subst. inversion H4. subst. inversion H1. destruct H2. destruct H2. inversion H5. destruct H2. destruct H2. inversion H5. subst. inversion H2. subst. lia. destruct H2. destruct H2. subst. inversion H4. + firstorder. subst. inversion H4. subst. inversion H4. subst. inversion H. subst. inversion H2. subst. inversion H4. inversion H. subst. inversion H. subst. inversion H4. * destruct x; auto. destruct y; subst. + inversion H. destruct H1. inversion H2. destruct H3. inversion H4. subst. clear H2 H4. inversion H3. destruct H2. destruct H2. subst. inversion H4. subst. inversion H1. destruct H2. destruct H2. inversion H5. destruct H2. destruct H2. inversion H5. subst. inversion H2. subst. destruct H2. destruct H2. subst. inversion H4. + destruct H. destruct H. inversion H1. destruct H2. inversion H3. subst. clear H1 H3. inversion H; clear H. destruct H1. destruct H. subst. inversion H. subst. clear H. inversion H2; clear H2. destruct H. destruct H. inversion H. destruct H. destruct H. inversion H. inversion H1. subst. lia. destruct H1. destruct H. inversion H. Qed.
imports: Coq(Relations Lia) AlmostFull.PropBounded(AlmostFull) AlmostFull.PropBounded(AlmostFullInduction) AlmostFull.PropBounded(AFConstructions)