proposition: Lemma opp_1: forall n v, In n v -> In (-n) (opp v).
proof: Proof. unfold In, opp; intros; cbn. replace (- - n) with n by lia. tauto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)