proposition: Lemma eq_nadd : forall (f g : nadd), dest_nadd f = dest_nadd g -> f = g.
proof: Proof. intros [f hf] [g hg]. simpl. intro e. subst g. apply subset_eq_compat. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance ExtensionalityFacts List Coq.Strings.Ascii