proposition: Lemma free_nullP : null \notin supp f -> null \notin supp (rem x f).
proof: Proof. by move=>H; rewrite supp_rem negb_and /= H orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)