proposition: Lemma add_repr: forall i i' bs bs', native_repr i bs -> native_repr i' bs' -> native_repr (add i i') (addB bs bs').
proof: Proof. move=> i i' ? ?. repeat (rewrite /native_repr eq_adj; move/eqP=> <-). apply/eqInt32P. move: i'; apply/(forallInt32P (fun i' => eq (add i i') (bitsToInt32 (addB (bitsFromInt32 i) (bitsFromInt32 i'))))). move=> i'; apply/eqInt32P. move: i; apply/forallInt32P; last by apply add_valid. move=> i'; apply idP. Qed.
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits)