proposition: Lemma nedouble_correct: forall sc n1 p1, n1 =~~= p1 -> [[ndouble sc n1]] -> fst (ndouble sc n1) =~~= add p1 p1.
proof: Proof. intros sc n1 p1 H; inversion_clear H. simpl; intros; constructor. intros V1. case (nInversible_double _ _ V1); intros V2 _. inversion_clear V2. simpl. case Kdec; [idtac | intros HH; case HH]; auto. intros e. match goal with |- context[?x ?= ?y] => generalize (is_zero_correct x y); case (Zeq_bool x y) end. intros HH; case Kdec. intros; constructor. intros HH1; case HH1; subst y1; rewrite HH. change (to_p 0) with pkO. field. intros HH2; apply inversible_kO with (2 := HH2); itac. intros HH1. assert (N1: inversible N y). inversion V1. generalize H3; generalize (Zeq_bool_eq y 0); case Zeq_bool. intros; case HH1; auto. intros; discriminate. generalize H3; case Zeq_bool; clear H3. intros; discriminate. intros HH; injection HH; clear HH. intros _ HH _ _; subst z0. repeat itac. assert (N2: to_p y <> pkO). intros HH; apply inversible_kO with (2 := HH); auto. assert (N3: to_p z <> pkO). intros HH; apply inversible_kO with (2 := HH); itac. case Kdec. intros HH; case N2. case (Kmult_integral pell_theory (1 + 1) y1). apply trans_equal with (y1 + y1); try ring. pattern y1 at 1; rewrite HH; ring. intros; case ptwo_not_zero; auto. intros; subst y1; field_simplify_eq in H3; auto. intros; simpl; constructor; to_p_tac; subst x1 y1; fold pA; set (v3 := (1 + (1 + 1))); set (v2 := (1 + 1)); field; repeat split; auto; apply ptwo_not_zero. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod