proposition: Lemma zeroTruncateK extra n p q : zeroTruncate extra (n:=n) p = Some q -> zeroExtend extra (n:=n) q = p.
proof: Proof. rewrite /zeroTruncate/zeroExtend. rewrite (split2eta p) split2app. case P: (high extra p == zero extra) => // H. have EQ: low n p = q by congruence. subst. by rewrite (eqP P). Qed.
imports: Coq(ZArith.ZArith) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple div zmodp ssralg) ssrextra.nat ssrextra.tuple spec.spec