proposition: Lemma size_domF k f : k \in dom f -> size (dom (free f k)) = (size (dom f)).-1.
proof: Proof. rewrite !umEX; case: (UMC.from f)=>[|f'] //=; case: f'=>f' F /= _. rewrite /supp /= !size_map size_filter=>H. move/(sorted_uniq (@trans K) (@irr K))/count_uniq_mem: F=>/(_ k). rewrite {}H count_map /ssrbool.preim /= => H. by rewrite -(count_predC [pred x | key x == k]) H addnC addn1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)