proposition: Lemma predkN (k1 k2 : K) : predI (predk V k1) (predCk V k2) =1 if k1 == k2 then pred0 else predk V k1.
proof: Proof. by move=>x; case: ifP=>H /=; [|case: eqP=>//->]; rewrite ?(eqP H) ?andbN ?H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)