proposition: Theorem length_flatten_nz : forall (A : Type)(ls : list (list A)) ls', In ls' ls -> length ls' > 0 -> length (flatten ls) > 0.
proof: Proof. induction ls; destruct ls'; intuition; simpl in *. lia. lia. intuition idtac; simpl in *; subst. rewrite app_length. simpl. lia. rewrite app_length. specialize (IHls (a0 :: ls') H1). simpl in *. intuition. lia. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation