moving forward.

High/curve_incl_Fp2.v

+Set Warnings "-notation-overridden,-parsing".
+From mathcomp Require Import ssreflect ssrbool eqtype div ssralg.
+From Tweetnacl.High Require Import mc.
+From Tweetnacl.High Require Import mcgroup.
+From Tweetnacl.High Require Import montgomery.
+From Tweetnacl.High Require Import curve25519.
+From Tweetnacl.High Require Import twist25519.
+From Tweetnacl.High Require Import opt_ladder.
+From Tweetnacl.High Require Import curve25519_prime.
+From Tweetnacl.High Require Import prime_ssrprime.
+From Reciprocity Require Import Reciprocity.Reciprocity.
+From Tweetnacl.High Require Import Zmodp2.
+From Tweetnacl.High Require Import Zmodp2_rules.
+From Tweetnacl.High Require Import curve25519_Fp2.
+From Tweetnacl.High Require Import curve25519_twist25519_eq.
+From Tweetnacl.High Require Import Zmodp.
+Require Import Ring.
+Require Import ZArith.
+
+Import BinInt.
+
+Open Scope ring_scope.
+Import GRing.Theory.
+
+Local Notation "p '#x0'" := (point_x0 p) (at level 30).
+Local Notation "Z.R A" := (Zmodp.repr A) (at level 30).
+Local Notation "-. A" := (Zmodp.opp A) (at level 30).
+
+(* Conversion between curve25519 over F_p and F_p2 *)
+Definition curve_Fp_to_Fp2 (p: point Zmodp.type) : (point Zmodp2.type) :=
+match p with
+  | EC_Inf => EC_Inf Zmodp2.type
+  | EC_In x y => EC_In (Zmodp2.Zmodp2 x 0) (Zmodp2.Zmodp2 y 0)
+end.
+
+Lemma oncurve25519_impl : forall (x y: Zmodp.type),
+oncurve curve25519_mcuType (EC_In x y) ->
+(oncurve curve25519_Fp2_mcuType (EC_In (Zmodp2.pi (x, Zmodp.pi 0)) (Zmodp2.pi (y, Zmodp.pi 0)))).
+Proof.
+move => x y /=.
+rewrite /a /b.
+rewrite ?expr2 ?expr3 ?expr3'.
+rewrite ?Zmodp2_mulE /= ?Zmodp2_addE /=.
+rewrite /curve25519.a /curve25519.b.
+ring_simplify_this.
+move/eqP => -> /=.
+apply/eqP.
+f_equal.
+Qed.
+
+Lemma on_curve_Fp_to_Fp2 : forall (p: point Zmodp.type),
+  oncurve curve25519_mcuType p -> oncurve curve25519_Fp2_mcuType (curve_Fp_to_Fp2 p).
+Proof.
+  move=> [|x y] => //.
+  apply oncurve25519_impl.
+Qed.
+
+Definition curve25519_Fp_to_Fp2 (p: mc curve25519_mcuType) : (mc curve25519_Fp2_mcuType) :=
+match p with
+  | MC u P => MC (on_curve_Fp_to_Fp2 u P)
+end.
+
+Local Lemma curve_add_Fp_to_Fp2 : forall (p q: point Zmodp_ringType) (p' q': point Zmodp2_ringType),
+  p' = curve_Fp_to_Fp2 p ->
+  q' = curve_Fp_to_Fp2 q ->
+  MCGroup.add curve25519_Fp2_mcuType p' q' = curve_Fp_to_Fp2 (MCGroup.add curve25519_mcuType p q).
+Proof.
+  move => [|xp yp] [|xq yq] [|xp' yp'] [|xq' yq'] //= [] -> -> [] -> ->.
+  rewrite /curve25519.a /curve25519.b.
+  match goal with
+    | [ |- _ = ?A ] => remember A as Freezer
+  end.
+  rewrite /eq_op /Equality.op /=.
+  rewrite /eq_op /Equality.op /=.
+  rewrite !eq_refl ?Bool.andb_true_r.
+  rewrite ?expr2.
+  have ->: 2%:R = Zmodp2.Zmodp2 (2%:R) 0 => //.
+  have ->: 3%:R = Zmodp2.Zmodp2 (3%:R) 0 => //.
+  Zmodpify => /=.
+  ringify.
+  subst Freezer.
+  ring_simplify_this.
+  case_eq (xp == xq) => -> //=.
+  case_eq ((yp == yq) && (yp != 0)) => -> //=.
+Qed.
+
+Local Lemma on_curve_add_Fp_to_Fp2 : forall (p q: point Zmodp_ringType),
+  oncurve curve25519_mcuType p ->
+  oncurve curve25519_mcuType q ->
+   oncurve curve25519_Fp2_mcuType (curve_Fp_to_Fp2 (MCGroup.add curve25519_mcuType p q)).
+Proof.
+  move=> p q Hp Hq.
+  pose p' := curve_Fp_to_Fp2 p.
+  pose q' := curve_Fp_to_Fp2 q.
+  rewrite -(curve_add_Fp_to_Fp2 p q p' q') => //.
+  have OCp' : oncurve curve25519_Fp2_mcuType p' by subst p' ; apply on_curve_Fp_to_Fp2.
+  have OCq' : oncurve curve25519_Fp2_mcuType q' by subst q' ; apply on_curve_Fp_to_Fp2.
+  by apply MCGroup.addO'.
+Qed.
+
+Lemma on_curve25519_add_Fp_to_Fp2: forall (p q: mc curve25519_mcuType),
+  oncurve curve25519_Fp2_mcuType (curve25519_Fp_to_Fp2 (p + q)).
+Proof.
+  by move => [p Hp] [q Hq] => /=; apply on_curve_add_Fp_to_Fp2.
+Qed.
+
+
+Local Lemma curve25519_add_Fp_to_Fp2' : forall (p q: mc curve25519_mcuType) (p' q': mc curve25519_Fp2_mcuType),
+  p' = curve25519_Fp_to_Fp2 p ->
+  q' = curve25519_Fp_to_Fp2 q ->
+  MCGroup.add curve25519_Fp2_mcuType p' q' = curve_Fp_to_Fp2 (MCGroup.add curve25519_mcuType p q).
+Proof.
+  move => [p Hp] [q Hq] [p' Hp'] [q' Hq'] Hpp' Hqq'.
+  apply curve_add_Fp_to_Fp2.
+  by simpl in Hpp'; inversion Hpp'.
+  by simpl in Hqq'; inversion Hqq'.
+Qed.
+
+Lemma curve25519_add_Fp_to_Fp2: forall (p q: mc curve25519_mcuType),
+  curve25519_Fp_to_Fp2 p + curve25519_Fp_to_Fp2 q = curve25519_Fp_to_Fp2 (p + q).
+Proof.
+  move => p q.
+  have [p' Hp']: exists (p': mc curve25519_Fp2_mcuType), p' = curve25519_Fp_to_Fp2 p by exists (curve25519_Fp_to_Fp2 p).
+  have [q' Hq']: exists (q': mc curve25519_Fp2_mcuType), q' = curve25519_Fp_to_Fp2 q by exists (curve25519_Fp_to_Fp2 q).
+  rewrite /GRing.add /=.
+  apply mc_eq.
+  rewrite -(curve25519_add_Fp_to_Fp2' _ _ _ _ Hp' Hq') Hp' Hq'.
+  reflexivity.
+Qed.
+
+Lemma nP_is_nP2 : forall (n:nat) (p: mc curve25519_mcuType),
+  curve25519_Fp_to_Fp2 (p *+ n) = (curve25519_Fp_to_Fp2 p) *+n.
+Proof.
+  elim => [|n IHn] p.
+  rewrite ?GRing.mulr0n => /=.
+  exact: mc_eq.
+  by rewrite ?GRing.mulrS -IHn curve25519_add_Fp_to_Fp2.
+Qed.
+
+Definition cFp_to_Fp2 p := match p with
+  | Zmodp2.Zmodp2 x y => x
+  end.
+
+Lemma cFp_to_Fp2_cancel : forall p: mc curve25519_mcuType,
+  p#x0 = cFp_to_Fp2 ((curve25519_Fp_to_Fp2 p)#x0).
+Proof. by case ; case. Qed.
+
+Local Notation "p '/p'" := (cFp_to_Fp2 p) (at level 40).
+
+From mathcomp Require Import ssrnat.
+
+Theorem curve25519_ladder_really_ok (n : nat) x :
+    (n < 2^255)%nat -> x != 0 ->
+    forall (p  : mc curve25519_mcuType),
+    (curve25519_Fp_to_Fp2 p)#x0 /p = x -> curve25519_ladder n x = ((curve25519_Fp_to_Fp2 p) *+ n)#x0 /p.
+Proof.
+  move => Hn Hx p Hp.
+  have Hp' := cFp_to_Fp2_cancel p.
+  have Hp'' : p #x0 = x.
+  by rewrite Hp'.
+  rewrite (curve25519_ladder_ok n x Hn Hx p Hp'').
+  rewrite -nP_is_nP2.
+  rewrite cFp_to_Fp2_cancel //.
+Qed.
+
+Close Scope ring_scope.
\ No newline at end of file

High/curve_twist_incl_Fp2.v

@@ -13,12 +13,12 @@ From Tweetnacl.High Require Import Zmodp2.
 From Tweetnacl.High Require Import Zmodp2_rules.
 From Tweetnacl.High Require Import curve25519_Fp2.
 From Tweetnacl.High Require Import curve25519_twist25519_eq.
+From Tweetnacl.High Require Import curve_incl_Fp2.
+From Tweetnacl.High Require Import twist_incl_Fp2.
 From Tweetnacl.High Require Import Zmodp.
 Require Import Ring.
 Require Import ZArith.
 
-(* Import BinInt. *)
-
 Open Scope ring_scope.
 Import GRing.Theory.
 
@@ -38,21 +38,6 @@ Proof.
   f_equal; f_equal; apply/eqP ; zmodp_compute => //=.
 Qed.
 
-Lemma oncurve25519_impl : forall (x y: Zmodp.type),
-oncurve curve25519_mcuType (EC_In x y) ->
-(oncurve curve25519_Fp2_mcuType (EC_In (Zmodp2.pi (x, Zmodp.pi 0)) (Zmodp2.pi (y, Zmodp.pi 0)))).
-Proof.
-move => x y /=.
-rewrite /a /b.
-rewrite ?expr2 ?expr3 ?expr3'.
-rewrite ?Zmodp2_mulE /= ?Zmodp2_addE /=.
-rewrite /curve25519.a /curve25519.b.
-ring_simplify_this.
-move/eqP => -> /=.
-apply/eqP.
-f_equal.
-Qed.
-
 Local Lemma oncurve25519 : forall x k k0 : Zmodp.type,
 curve25519.b * k0 ^+ 2 == k ^+ 3 + curve25519.a * k ^+ 2 + k ->
 k = x -> exists p0 : mc curve25519_Fp2_mcuType, p0 #x0 = Zmodp2.Zmodp2 x 0.
@@ -64,21 +49,6 @@ exists (MC HOC) => /=.
 have ->: Zmodp.pi 0 = Zmodp.zero => //=.
 Qed.
 
-Lemma ontwist25519_impl : forall (x y: Zmodp.type),
-oncurve twist25519_mcuType (EC_In x y) ->
-(oncurve curve25519_Fp2_mcuType (EC_In (Zmodp2.pi (x, Zmodp.pi 0)) (Zmodp2.pi (Zmodp.pi 0, y)))).
-Proof.
-move => x y /=.
-rewrite /a /b.
-rewrite ?expr2 ?expr3 ?expr3'.
-rewrite ?Zmodp2_mulE /= ?Zmodp2_addE /=.
-rewrite /twist25519.a /twist25519.b.
-ring_simplify_this.
-move/eqP => -> /=.
-apply/eqP.
-f_equal.
-Qed.
-
 Local Lemma ontwist25519 : forall x k k0 : Zmodp.type,
 twist25519.b * k0 ^+ 2 == k ^+ 3 + twist25519.a * k ^+ 2 + k ->
 k = x -> exists p0 : mc curve25519_Fp2_mcuType, p0 #x0 = Zmodp2.Zmodp2 x 0.
@@ -103,198 +73,60 @@ Proof.
   - apply ontwist25519.
 Qed.
 
-Definition curve_Fp_to_Fp2 (p: point Zmodp.type) : (point Zmodp2.type) :=
-match p with
-  | EC_Inf => EC_Inf Zmodp2.type
-  | EC_In x y => EC_In (Zmodp2.Zmodp2 x 0) (Zmodp2.Zmodp2 y 0)
-end.
-
-Definition twist_Fp_to_Fp2 (p: point Zmodp.type) : (point Zmodp2.type) :=
-match p with
-  | EC_Inf => EC_Inf Zmodp2.type
-  | EC_In x y => EC_In (Zmodp2.Zmodp2 x 0) (Zmodp2.Zmodp2 0 y)
-end.
-
-Lemma curve_add_Fp_to_Fp2 : forall (p q: point Zmodp_ringType) (p' q': point Zmodp2_ringType),
-  p' = curve_Fp_to_Fp2 p ->
-  q' = curve_Fp_to_Fp2 q ->
-  MCGroup.add_no_check curve25519_Fp2_mcuType p' q' = curve_Fp_to_Fp2 (MCGroup.add_no_check curve25519_mcuType p q).
-Proof.
-  move => [|xp yp] [|xq yq] [|xp' yp'] [|xq' yq'] //= [] -> -> [] -> ->.
-  rewrite /curve25519.a /curve25519.b.
-  match goal with
-    | [ |- _ = ?A ] => remember A as Freezer
-  end.
-  rewrite /eq_op /Equality.op /=.
-  rewrite /eq_op /Equality.op /=.
-  rewrite !eq_refl ?Bool.andb_true_r.
-  rewrite ?expr2.
-  have ->: 2%:R = Zmodp2.Zmodp2 (2%:R) 0 => //.
-  have ->: 3%:R = Zmodp2.Zmodp2 (3%:R) 0 => //.
-  Zmodpify => /=.
-  ringify.
-  subst Freezer.
-  ring_simplify_this.
-  case_eq (xp == xq) => -> //=.
-  case_eq ((yp == yq) && (yp != 0)) => -> //=.
-Qed.
-
-Lemma twist_add_Fp_to_Fp2 : forall (p q: point Zmodp_ringType) (p' q': point Zmodp2_ringType),
-  p' = twist_Fp_to_Fp2 p ->
-  q' = twist_Fp_to_Fp2 q ->
-  MCGroup.add_no_check curve25519_Fp2_mcuType p' q' = twist_Fp_to_Fp2 (MCGroup.add_no_check twist25519_mcuType p q).
-Proof.
-  move => [|xp yp] [|xq yq] [|xp' yp'] [|xq' yq'] //= [] -> -> [] -> ->.
-  rewrite /twist25519.a /twist25519.b.
-  match goal with
-    | [ |- _ = ?A ] => remember A as Freezer
+Definition Fp_to_Fp2 p := match p with
+  | Zmodp2.Zmodp2 x y => x
   end.
-  rewrite /eq_op /Equality.op /=.
-  rewrite /eq_op /Equality.op /=.
-  rewrite !eq_refl ?Bool.andb_true_r.
-  rewrite ?expr2.
-  have ->: 2%:R = Zmodp2.Zmodp2 (2%:R) 0 => //.
-  have ->: 3%:R = Zmodp2.Zmodp2 (3%:R) 0 => //.
-  Zmodpify => /=.
-  subst Freezer.
-  ringify.
-  ring_simplify_this.
-  case_eq (xp == xq) => -> ; rewrite -Zmodp_mul_comm_2 ?GRing.mulrA //=.
-  case_eq ((yp == yq) && (yp != 0)) => -> //=.
-Qed.
-
-
-
 
-(* a great definition ... *)
-(* Definition curve_to_Fp2 (p: mc curve25519_mcuType) : (mc curve25519_Fp2_mcuType) :=
-match p with
-  | MC u P =>
-  match u, P with 
-  | EC_Inf, _ => MC (MCGroup.zeroO curve25519_Fp2_mcuType)
-  | EC_In x y, P => MC (oncurve25519_impl x y P)
-  end
-end.
- *)
-(* a not so great definition ... *)
+Lemma Fp_to_Fp2_t : forall p:mc twist25519_mcuType,
+  p#x0 = Fp_to_Fp2 ((twist25519_Fp_to_Fp2 p)#x0).
+Proof. by case; case. Qed.
 
-(* 
-Lemma curve_to_Fp2_inf : curve_to_Fp2 (MC (MCGroup.zeroO curve25519_mcuType)) = MC (MCGroup.zeroO curve25519_Fp2_mcuType).
-Proof. done. Qed.
-*)
-(* Lemma curve_to_Fp2_xy x y (P: oncurve curve25519_mcuType (|x , y|)): curve_to_Fp2 (MC P) = MC (oncurve25519_impl x y P).
-Proof. done. Qed.
- *)
-(* a not so great definition ... *)
-(* Definition curve_to_Fp2 (p: point Zmodp.type) : (point Zmodp2.type) :=
-match p with
-  | EC_Inf => EC_Inf Zmodp2.type
-  | EC_In x y => EC_In (Zmodp2.Zmodp2 x 0) (Zmodp2.Zmodp2 y 0)
-end.
- *)
-(* a great definition ... *)
-(* Definition twist_to_Fp2 (p: mc twist25519_mcuType) : (mc curve25519_Fp2_mcuType) :=
-match p with
-  | MC (EC_Inf) _ => MC oncurve_inf
-  | MC (EC_In x y) P => MC (ontwist25519_impl x y P)
-end.
- *)
-(* a not so great definition ... *)
-(* Definition twist_to_Fp2 (p: point Zmodp.type) : (point Zmodp2.type) :=
-match p with
-  | EC_Inf => EC_Inf Zmodp2.type
-  | EC_In x y => EC_In (Zmodp2.Zmodp2 x 0) (Zmodp2.Zmodp2 0 y)
-end.
- *)
+Lemma Fp_to_Fp2_c : forall p:mc curve25519_mcuType,
+  p#x0 = Fp_to_Fp2 ((curve25519_Fp_to_Fp2 p)#x0).
+Proof. by case; case. Qed.
 
+Lemma Fp_to_Fp2_eq_C: Fp_to_Fp2 = cFp_to_Fp2.
+Proof. reflexivity. Qed.
 
+Lemma Fp_to_Fp2_eq_T: Fp_to_Fp2 = tFp_to_Fp2.
+Proof. reflexivity. Qed.
 
+From mathcomp Require Import ssrnat.
+Local Notation "p '/p'" := (Fp_to_Fp2 p) (at level 40).
 
-(* Lemma nP_is_nP2 : forall (x1 x2 xs: Zmodp.type),
-  forall (p1 : mc curve25519_mcuType), p1#x0 = x1 ->
-  forall (p2 : mc curve25519_mcuType), p2#x0 = x2 ->
-  (p1 + p2)#x0 = xs ->
-
-  forall (p'1: mc curve25519_Fp2_mcuType), p'1#x0 = Zmodp2.Zmodp2 x1 0 ->
-  forall (p'2: mc curve25519_Fp2_mcuType), p'2#x0 = Zmodp2.Zmodp2 x2 0 ->
-  (p'1 + p'2)#x0 = Zmodp2.Zmodp2 xs 0.
+Lemma curve25519_ladder_maybe_ok (n : nat) x :
+    (n < 2^255)%nat -> x != 0 ->
+    forall (p'  : mc curve25519_Fp2_mcuType),
+    (exists p, curve25519_Fp_to_Fp2 p #x0 /p = x) \/ (exists p, twist25519_Fp_to_Fp2 p #x0 /p = x) ->
+    p'#x0 /p = x -> curve25519_ladder n x = (p' *+ n)#x0 /p.
 Proof.
+  move => Hn Hx p' [[p Hp]|[p Hp]] Hp'.
+(*   have [[p Hp]|[p Hp]]:= x_is_on_curve_or_twist x. *)
+  rewrite (curve25519_ladder_really_ok n x Hn Hx p Hp) -Fp_to_Fp2_eq_C.
+  f_equal.
+  f_equal.
+  f_equal.
+  f_equal.
+  destruct p, p' => /=.
+  apply mc_eq.
+  destruct p, p0 => //=.
+  move: Hp Hp' Hx => /= <- //=.
+  move: Hp Hp' Hx => /= <- <- //=.
+  move: Hp Hp' => /= -> <-.
 Admitted.
- *)
-(*   move=> x1 x2 xs [p1 OCp1] Hp1
-  [p2 OCp2] Hp2
-  [p'1 OCp'1] Hp'1
-  [p'2 OCp'2] Hp'2 /= ;
-  rewrite /MCGroup.add ?OCp1 ?OCp2 ?OCp'1 ?OCp'2.
-  move: p1 OCp1 Hp1 => [|xp1 yp1] OCp1 Hp1.
-  +{
-    move => <- //.
-    move: p'1 OCp'1 Hp'1 => [|xp'1 yp'1] OCp'1 Hp'1.
-    - move: Hp2 Hp'2 <- => //=.
-    - move: p'2 OCp'2 Hp'2 => [|xp'2 yp'2] OCp'2 Hp'2 //.
-      move: Hp1 Hp'1 <- => /= ->.
-      move: Hp2 Hp'2 => /= -> <- //=.
-      move: Hp1 Hp'1 => /= <- ->.
-      case_eq (Zmodp2.Zmodp2 0 0 == xp'2) => eq_xp'2 ; rewrite eq_xp'2 /=.
-      * move/eqP:eq_xp'2 => eq_xp'2.
-      case_eq ((yp'1 == yp'2) && (yp'1 != 0)) => eq2 ; rewrite eq2 /=.
-      rewrite (expr2 (Zmodp2.pi (0,0))).
-      rewrite ?GRing.mulr0.
-      rewrite ?GRing.add0r.
-      rewrite ?GRing.subr0.
-      move/andb_prop:eq2 => [].
-      move/eqP ->. move/eqP.
-      move=> Hyp'2.
-      move: Hp2 Hp'2 eq_xp'2 => /= -> ->.
-      move: OCp'2 => /=.
-      rewrite /b.
-      move/eqP.
-      rewrite ?GRing.mulr1.
-      rewrite ?GRing.mul1r.
-      move=>HP2 H2'.
-      inversion H2' as [H]; clear H2'.
-      move: H HP2. => <-.
-
-
 
+Theorem curve25519_ladder_really_ok (n : nat) (x:Zmodp.type) :
+    (n < 2^255)%nat -> x != 0 ->
+    forall (p'  : mc curve25519_Fp2_mcuType),
+    p'#x0 /p = x -> curve25519_ladder n x = (p' *+ n)#x0 /p.
+Proof.
+  have : (exists p, curve25519_Fp_to_Fp2 p #x0 /p = x) \/ (exists p, twist25519_Fp_to_Fp2 p #x0 /p = x).
+  have := (x_is_on_curve_or_twist x).
+  move => [[p Hp]|[p Hp]].
+  by left; exists p;  move: p Hp => [[| xp yp] Hp] /=.
+  by right; exists p;  move: p Hp => [[| xp yp] Hp] /=.
+  intros ; apply curve25519_ladder_maybe_ok => //.
+Qed.
 
-      SearchAbout (_ == _ = true).
-
-      move/andb_prop.
-      ring.
-      rewrite Zmodp2_mulE /=.
-
-      rewrite /GRing.mul /= /Zmodp2.mul /=.
-      zmodp_compute.
- ring.
-      reflexivity.
-      have: (if_spec (Zmodp2.Zmodp2 0 0 == xp'2)).
-      move: Hp2 Hp'2 => /= <-.
-      
-
-      
-  + move: 
-  + move => <- /=.
-    move: Hp'2 => /=.
-    move: Hp2 => /= <- //.
-  + move => <- /=.
-    move: Hp'1 => /=.
-    move: Hp1 => /= <- //.
- 
-  Search "_ + _".
-  rewrite /add.
-
- *)
 
-(* Lemma nP_is_nP2' : forall (n:nat) (x xn: Zmodp.type),
-  forall (p : mc curve25519_mcuType), p#x0 = x ->
-  forall (p': mc curve25519_Fp2_mcuType), p'#x0 = Zmodp2.Zmodp2 x 0 ->
-  (p *+ n)#x0 = xn ->
-  (p' *+ n)#x0 = Zmodp2.Zmodp2 xn 0.
-Proof.
-  elim => [|n IHn] x xn p Hp p' Hp'.
-  rewrite ?mulr0n /= => <- //.
-  rewrite GRing.mulrS.
-  rewrite GRing.mulrS.
-  elim (p *+ n).
-  SearchAbout "*+". *)
\ No newline at end of file
+Close Scope ring_scope.

High/mc.v

@@ -60,6 +60,15 @@ Section MC.
 
   Inductive mc : Type := MC p of oncurve p.
 
+  Lemma mc_eq : forall (p q: point K) Hp Hq,
+    p = q -> @MC p Hp = @MC q Hq.
+  Proof.
+    move => p q Hp Hq Heq.
+    subst p.
+    f_equal.
+    apply eq_irrelevance.
+  Qed.
+
   Coercion point_of_mc p := let: MC p _ := p in p.
 
   Canonical Structure mc_subType := [subType for point_of_mc by mc_rect].
@@ -157,7 +166,7 @@ Module MCGroup.
     Definition neg (p : point K) :=
       if p is (|x, y|) then (|x, -y|) else ∞.
 
-    Definition add (p1 p2 : point K) :=
+    Definition add_check (p1 p2 : point K) :=
       let p1 := if oncurve M p1 then p1 else ∞ in
       let p2 := if oncurve M p2 then p2 else ∞ in
 
@@ -179,7 +188,7 @@ Module MCGroup.
               (| xs, - s * (xs - x1) - y1 |)
         end.
 
-    Definition add_no_check (p1 p2 : point K) :=
+    Definition add (p1 p2 : point K) :=
         match p1, p2 with
         | ∞, _ => p2 | _, ∞ => p1
 
@@ -201,9 +210,9 @@ Module MCGroup.
     Lemma add_no_check_eq (p1 p2:point K) :
       oncurve M p1 ->
       oncurve M p2 ->
-      add_no_check p1 p2 = add p1 p2.
+      add p1 p2 = add_check p1 p2.
     Proof.
-      rewrite /add_no_check /add => -> -> //.
+      rewrite /add /add_check => -> -> //.
     Qed.
 
     Lemma zeroO : oncurve M ∞.
@@ -258,9 +267,9 @@ Module MCGroup.
                   (|x, y|)
         end.
 
-    Lemma ladd_addE p q: ladd p q = neg (add p q).
+    Lemma ladd_addE p q: ladd p q = neg (add_check p q).
     Proof.
-      rewrite /ladd /add;
+      rewrite /ladd /add_check;
         set pp := if oncurve M p then _ else _;
         set qq := if oncurve M q then _ else _.
       have oncve_pp: oncurve M pp by rewrite {}/pp; case h: (oncurve M p).
@@ -430,7 +439,7 @@ Module MCGroup.
     Lemma negK: involutive neg.
     Proof. by case=> [|x y] //=; rewrite opprK. Qed.
 
-    Lemma addO p q: oncurve M (add p q).
+    Lemma addO_check p q: oncurve M (add_check p q).
     Proof.
       rewrite oncurveN -ladd_addE /ladd;
         set pp := if oncurve M p then _ else _;
@@ -450,27 +459,31 @@ Module MCGroup.
       by rewrite !exprMn; congr (_ * _); rewrite -[c-_]opprK opprB sqrrN.
     Defined.
 
-    Lemma addO' (p q: mc M): oncurve M (add_no_check p q).
+    Lemma addO' p q: oncurve M p -> oncurve M q -> oncurve M (add p q).
     Proof.
-    destruct p as [p Hp], q as [q Hq].
+    move => Hp Hq.
     rewrite (add_no_check_eq Hp Hq).
-    apply addO.
+    apply addO_check.
     Qed.
 
-    Lemma add0o : {in (oncurve M), left_id ∞ add}.
+    Lemma addO (p q: mc M): oncurve M (add p q).
     Proof.
-      move=> p; rewrite /in_mem /= => oncve_p.
-      by rewrite /add /= oncve_p.
+    destruct p as [p Hp], q as [q Hq].
+    by apply addO'.
     Qed.
 
-    Lemma add0o' : {in (oncurve M), left_id ∞ add_no_check}.
+    Lemma add0o_check : {in (oncurve M), left_id ∞ add_check}.
     Proof.
-      done.
+      move=> p; rewrite /in_mem /= => oncve_p //.
+      by rewrite /add_check /= oncve_p.
     Qed.
 
-    Lemma addNo : left_inverse ∞ neg add.
+    Lemma add0o : {in (oncurve M), left_id ∞ add}.
+    Proof. done. Qed.
+
+    Lemma addNo_check : {in (oncurve M), left_inverse ∞ neg add_check}.
     Proof.
-      move=> p; rewrite /add -oncurveN.
+      move=> p; rewrite /add_check -oncurveN.
       have [|] := (boolP (oncurve M p)) => // _.
       case: p=> [|x y] //=; rewrite eqxx /= eq_sym; case Hy0: (y == 0).
       + by rewrite (eqP Hy0) oppr0 eqxx //.
@@ -478,18 +491,18 @@ Module MCGroup.
         by absurd false=> //; rewrite -Hy0 -eqrN_eq0 HyN.
     Qed.
 
-    Lemma addNo' : {in (oncurve M), left_inverse ∞ neg add_no_check}.
+    Lemma addNo : {in (oncurve M), left_inverse ∞ neg add}.
     Proof.
       move=> p.
       rewrite /in_mem /mem => /= Hp.
       rewrite add_no_check_eq //.
       2: rewrite -oncurveN //.
-      apply addNo.