proposition: Lemma catB_inj n1 n2 (p1 q1: BITS n1) (p2 q2: BITS n2) : p1 ## p2 = q1 ## q2 -> p1 = q1 /\ p2 = q2.
proof: Proof. move => EQ. have H1 := high_catB p1 p2. have H2 := high_catB q1 q2. have L1 := low_catB p1 p2. have L2 := low_catB q1 q2. split. by rewrite -H1 -H2 EQ. by rewrite -L1 -L2 EQ. 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