proposition: Lemma testbit_adccarries_pos x y c i (Hi : 0 < i) : Z.testbit (adccarries x y c) i = (x.[i-1] && y.[i-1] || (x.[i-1]^^y.[i-1]) && (adccarries x y c).[i-1])%bool.
proof: Proof. pose proof shiftr_adccarries_1 x y c. apply (f_equal (fun x => Z.testbit x (i-1))) in H. autorewrite with bitwise in H; rewrite <-H. rewrite Z.shiftr_spec; try lia. f_equal; lia. Qed.
imports: BinInt Lia Btauto