proposition: Lemma sqrtrem_step_spec f g p x : (f=xO \/ f=xI) -> (g=xO \/ g=xI) -> SqrtSpec p x -> SqrtSpec (sqrtrem_step f g p) (g (f x)).
proof: Proof. intros Hf Hg [ s _ -> | s r _ -> Hr ]. - unfold sqrtrem_step. destruct Hf,Hg; subst; simpl; constructor; now rewrite ?square_xO. - assert (Hfg : forall p q, g (f (p+q)) = p~0~0 + g (f q)) by (intros; destruct Hf, Hg; now subst). unfold sqrtrem_step, leb. case compare_spec; [intros EQ | intros LT | intros GT]. + rewrite <- EQ, sub_mask_diag. constructor. destruct Hg; subst g; destr_eq EQ. destruct Hf; subst f; destr_eq EQ. subst. now rewrite square_xI. + destruct (sub_mask_pos' _ _ LT) as (y & -> & H). constructor. * rewrite Hfg, <- H. now rewrite square_xI, add_assoc. * clear Hfg. rewrite <- lt_succ_r in Hr. change (r < s~1) in Hr. rewrite <- lt_succ_r, (add_lt_mono_l (s~0~1)), H. simpl. rewrite add_carry_spec, add_diag. simpl. destruct Hf,Hg; subst; red; simpl_compare; now rewrite Hr. + constructor. * now rewrite Hfg, square_xO. * apply lt_succ_r, GT. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef