proposition: Lemma toZp_adcB n b (p1 p2:BITS n) : toZp (adcBmain b p1 p2) = (bool_inZp _ b + toZpAux p1 + toZpAux p2)%R.
proof: Proof. apply val_inj. rewrite /= Zp_cast; last apply pow2_gt1. rewrite toNat_adcBmain. have BOUND:= adcB_bounded b p1 p2. rewrite modn_small => //. rewrite (@modn_small b). rewrite (@modn_small (toNat p1)). rewrite (@modn_small (toNat p2)). rewrite (@modn_small (b + toNat p1)). rewrite modn_small => //. apply: leq_ltn_trans BOUND. apply leq_addr. apply: leq_ltn_trans BOUND. rewrite addnC. apply leq_addr. apply: leq_ltn_trans BOUND. rewrite -addnAC. apply leq_addl. apply: leq_ltn_trans BOUND. rewrite -addnA. apply leq_addr. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations mathcomp(ssralg)