proposition: Lemma in_dunit t t' : t' \in dinsupp (dunit t) -> t' = t :> T.
proof: Proof. by rewrite in_dinsupp dunit1E pnatr_eq0 eqb0 negbK => /eqP. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum