proposition: Lemma cdisjoint_plift_perfect m c : cdisjoint (plift c) `c[i, m].
proof: Proof. apply/cdisjointP=> i1 j1; rewrite !ffunE /p; apply/eqP/val_eqP => /=. by rewrite eq_sym neq_bump. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)