proposition: Lemma neadd_correct: forall sc n1 p1 n2 p2, n1 =~~= p1 -> n2 =~~= p2 -> [[nadd sc n1 n2]] -> fst (nadd sc n1 n2) =~~= add p1 p2.
proof: Proof. intros sc n1 p1 n2 p2 H; inversion_clear H. simpl; auto. intros H; inversion_clear H. simpl; intros; constructor; auto. intros V1. case (nInversible_add _ _ _ V1); intros V2 (V3, _). inversion_clear V2. inversion_clear V3. repeat itac. simpl. assert (F0:= (inversible_is_not_k0 NI2)). assert (F0b:= (inversible_is_not_k0 NI0)). generalize V1; simpl. repeat match goal with |- context[?x ?= ?y] => generalize (is_zero_correct x y); case (Zeq_bool x y) end; repeat case Kdec; auto. intros; constructor. intros n e K1 K2 K3 U1; subst y. match type of K2 with ?X = 0%Z => cut ((to_p X) = pkO); [idtac | rewrite K2; auto]; to_p_tac; clear K2; intros K2 end. case (Kmult_integral pell_theory (to_p y0) (to_p z)); auto. rewrite <- K2; change (to_p 0) with pkO; ring. intros HH; case n; subst y1 y2; rewrite HH; auto. intros; case F0; auto. intros n K1 K2 K3 U1. case n; subst x1 x2. field_simplify_eq; auto. match type of K3 with ?X = 0%Z => cut ((to_p X) = pkO); [idtac | rewrite K3; auto]; to_p_tac; clear K3; intros K3 end. match goal with |- ?X = _ => apply trans_equal with (X + pkO); try ring end. rewrite <- K3; ring. intros K1 K2 K3 K4 _ U1; subst y1 y2. match type of K4 with ?X = 0%Z => cut ((to_p X) = pkO); [idtac | rewrite K4; auto]; to_p_tac; clear K4; intros K4 end. field_simplify_eq in K1; auto. rewrite K1 in K4. case (Kmult_integral pell_theory (1 + 1) (to_p z * to_p y0)); auto. set (u := to_p z * to_p y0) in * |- *. apply trans_equal with (u + u); try ring. unfold u; rewrite <- K4; ring. intros; case ptwo_not_zero; auto. intros HH; case (Kmult_integral pell_theory _ _ HH); clear HH; intros HH. case F0; auto. rewrite HH in K1; ring_simplify in K1. case (Kmult_integral pell_theory (to_p y) (to_p z0)); auto. intros HH1. inversion_clear U1. repeat itac; auto. case (@inversible_is_not_k0 y); auto. intros; case F0b; auto. intros. assert (VV: to_p y <> pkO). apply inversible_is_not_k0. inversion_clear V0. repeat itac; auto. intros; simpl fst; 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. intros n K1 K2 K3; case n; subst x1 x2. field_simplify_eq; auto. match type of K3 with ?X = 0%Z => cut ((to_p X) = pkO); [idtac | rewrite K3; auto]; to_p_tac; clear K3; intros K3 end. apply trans_equal with (to_p z * to_p x0 - pkO); try ring. rewrite <- K3; try ring. intros; simpl fst; constructor. intros n K1 K2 K3 K4. inversion K4. repeat itac. case (inversible_is_not_k0 NI3). to_p_tac. rewrite <- K1 in H3. rewrite <- H3 in H0; simpl in H0. case (Kmult_integral pell_theory (y1 + y2) (y1 - y2)). ring [H0]. intros HH; case n. apply trans_equal with (y1 - pkO); try ring; rewrite <- HH; ring. intros HH; subst y1 y2. assert (HH1:= Keq_minus_eq pell_theory _ _ HH). field_simplify_eq in HH1; auto. change (znz p) with pK; ring [HH1]. intros n K1 K2 K3. case n; subst x1 x2; field_simplify_eq; auto. match type of K2 with ?X = 0%Z => cut ((to_p X) = pkO); [idtac | rewrite K2; auto]; to_p_tac; clear K2; intros K2 end. assert (HH1:= Keq_minus_eq pell_theory _ _ K2); auto. ring [HH1]. intros K1 K2 K3 K4. inversion_clear K4. repeat itac. case (inversible_is_not_k0 NI6). to_p_tac. apply (Keq_minus_eq_inv pell_theory). subst x1 x2; field_simplify_eq in K2; auto; ring [K2]. intros K1 K2 K3 K4. inversion_clear K4. repeat itac. case (inversible_is_not_k0 NI6). to_p_tac. apply (Keq_minus_eq_inv pell_theory). subst x1 x2; field_simplify_eq in K2; auto; ring [K2]. intros; simpl; constructor; to_p_tac; subst y2 x2 y1 x1; field; repeat split; auto. intros H1; case n; field_simplify_eq; auto. ring [(Keq_minus_eq pell_theory _ _ H1)]; auto. inversion_clear V0. repeat itac. intros H2; case (inversible_is_not_k0 NI6). to_p_tac. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod