proposition: Theorem length_getUnique_nz : forall (A :Set)(eqd : eq_dec A)(ls : list A), length ls > 0 -> length (getUnique ls eqd) > 0.
proof: Proof. induction ls; intuition; simpl in *. destruct (in_dec eqd a (getUnique ls eqd)). destruct ls; simpl in *; intuition. simpl. lia. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation