proposition: Theorem pe2e_double: forall p1, pe2e (pdouble p1) = add (pe2e p1) (pe2e p1).
proof: Proof. intros (x1,y1,z1,H1). unfold pdouble, pe2e. case wb; intros b; case b; intros Hb; clear b. rewrite Hb; auto. case wb; intros b; case b; intros Hz1; clear b; auto. apply False_ind; rewrite Hb in Hz1; discriminate. replace (z1 ?0) with false. unfold add. generalize (is_zero_false Hb); intros Hz1. repeat ksplit. generalize (Keq_minus_eq_inv KD0); clear KD0; intros KD0. field_simplify_eq in KD0; auto. case (Kmult_integral KD0); auto; clear KD0; intro KD0. case Kdiff_2_0; auto. subst y1. case wb; intros b; case b; intros Hb1; clear b; auto. case (is_zero_false Hb1); field; auto. case wb; intros b; case b; intros Hb1; clear b; auto. case (Kmult_integral (is_zero_true Hb1)); intros V1. case Hz1; auto. assert (V2: 2 * y1 * z1 = 0). case (Kmult_integral V1); clear V1; intros V1; auto. case (Kmult_integral V1); clear V1; intros V1; auto. case (Kmult_integral V2); clear V2; intros V2. case (Kmult_integral V2); clear V2; intros V2. case Kdiff_2_0; auto. case KD0; field[V2]; auto. case KD0; field[V2]; auto. generalize (is_zero_false Hb1); intros zH. apply curve_elt_irr; field; repeat (split; auto). intros HH; case zH; ring [HH]. intros HH; case zH; ring [HH]. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith