proposition: Lemma is_nadd_0 : is_nadd (fun _ => 0).
proof: Proof. unfold is_nadd. exists 0. intros m n. simpl. repeat rewrite mul_0_r. rewrite dist_refl. auto. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance ExtensionalityFacts List Coq.Strings.Ascii