proposition: Lemma pickleP : (pcancel picklef unpicklef) /\ (pcancel picklep unpicklep).
proof: Proof. apply: form_prog_ind => //= *; by repeat match goal with [ H : _ = Some _ |- _] => rewrite ?H /= => {H} end. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)