proposition: Theorem app_eq_inv : forall (A : Type)(ls1 ls2 ls3 ls4 : list A), length ls1 = length ls3 -> (ls1 ++ ls2) = (ls3 ++ ls4) -> ls1 = ls3 /\ ls2 = ls4.
proof: Proof. induction ls1; destruct ls3; intros; simpl in *; subst. intuition. lia. lia. inversion H0; clear H0; subst. specialize (IHls1 ls2 ls3 ls4). intuition. f_equal. eapply IHls1; intuition; lia. eapply IHls1; intuition; lia. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation