proposition: Lemma testbit_addcarries_pos x y i (Hi : 0 < i) : Z.testbit (addcarries x y) i = (x.[i-1] && y.[i-1] || (x.[i-1]^^y.[i-1]) && (addcarries x y).[i-1])%bool.
proof: Proof. rewrite addcarries_ok; apply testbit_adccarries_pos, Hi. Qed.
imports: BinInt Lia Btauto