proposition: Theorem pe2e_add: forall p1 p2, pe2e (padd p1 p2) = add (pe2e p1) (pe2e p2).
proof: Proof. intros (x1,y1,z1,H1) (x2,y2,z2,H2). unfold padd, pe2e. case wb; intros b; case b; intros Hb; clear b. rewrite Hb; auto. replace (z1 ?0) with false. case wb; intros b; case b; intros Hb1; clear b. rewrite Hb1; auto. case wb; intros b; case b; intros Hb2; clear b; auto. rewrite Hb in Hb2; discriminate. simpl; apply curve_elt_irr; auto. replace (z2 ?0) with false. assert (F1 := is_zero_false Hb). assert (F2 := is_zero_false Hb1). unfold add. case Kdec; intros HH1; apply sym_equal; case Kdec; intros HH2; apply sym_equal. 2: case HH2; apply Keq_minus_eq; field_simplify_eq; auto; apply trans_equal with (-0); try ring; rewrite <- HH1; ring. 2: case HH1; apply trans_equal with (x2/z2 * z2 * z1 - x1 * z2); try (field; auto); rewrite <- HH2; field; auto. ksplit; symmetry; ksplit. generalize (Keq_minus_eq_inv KD0); clear KD0; intros KD0. field_simplify_eq in KD0; auto. rewrite <- KD in KD0. generalize (Keq_minus_eq_inv KD0); clear KD0; intros KD0. field_simplify_eq in KD0; auto. case (Kmult_integral KD0); clear KD0; intros KD0; auto. 2: case F2; auto. case (Kmult_integral KD0); clear KD0; intros KD0; auto. case Kdiff_2_0; auto. case wb; intros b; case b; intros Hb2; auto. case (is_zero_false Hb2). ring [KD0]. assert (HH: y1 <> 0). intros HH. ring_simplify [HH] in KD. case (Kmult_integral KD); clear KD; intros KD; auto. case KD0; field [HH KD]; auto. case wb; intros b; case b; intros Hb2; auto. assert (F3 := is_zero_true Hb2). assert (V1: 2 * y1 * z1 = 0). case (Kmult_integral F3); clear F3; intros V1; auto. case F1; auto. case (Kmult_integral V1); clear V1; intros V1; auto. case (Kmult_integral V1); clear V1; intros V1; auto. case (Kmult_integral V1); clear V1; intros V1; auto. case (Kmult_integral V1); clear V1; intros V1; auto. case Kdiff_2_0; auto. case HH; auto. case F1; auto. apply curve_elt_irr; field; repeat (split; auto). case wb; intros b; case b; intros Hb2; auto. case (is_zero_false Hb2); auto. case (@curve_elt_opp (x1/z1) (x2/z2) (y1/z1) (y2/z2) (pe2e_lem1 H1 Hb) (pe2e_lem1 H2 Hb1)); auto; intros tmp; injection tmp; intros HH _. generalize (Keq_minus_eq_inv HH); clear HH; intros HH. field_simplify_eq in HH; auto. case KD; symmetry; apply Keq_minus_eq; apply trans_equal with (2 := HH). case KD; symmetry; apply Keq_minus_eq; apply trans_equal with (2 := HH). ring. case KD0; auto. case wb; intros b; case b; intros Hb2; auto. assert (F3 := is_zero_true Hb2). case HH1. case (Kmult_integral F3); clear F3; intros V1; auto. case (Kmult_integral V1); clear V1; intros V1; auto. case F1; auto. case F2; auto. case (Kmult_integral V1); clear V1; intros V1; auto. case (Kmult_integral V1); clear V1; intros V1; auto. apply curve_elt_irr; field; repeat (split; auto). Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith