proposition: Lemma adcIsIterInc n m : forall c (p:BITS n), dropmsb (adcBmain c p #m) = iter m incB (if c then incB p else p).
proof: Proof. induction m => c p. + by rewrite /= adcIsInc. + rewrite /= -IHm. clear IHm. rewrite 2!adcBmain_nat. rewrite !dropmsb_fromNat. set D := c + toNat p. rewrite incB_fromNat. rewrite -(addn1 (D + toNat #m)) -addnA. apply fromNat_addn. rewrite toNatK addn1. apply fromNat_succn. by rewrite toNatK. 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)