why-bundle.v

  Check 
    Algebra.Group.is_homomorphism
    (G:=E.point(F:=F q)(Feq:=Logic.eq)(Fone:=1%F)(Fadd:=F.add)(Fmul:=F.mul)
               (a:=SpecEd25519.a)(d:=SpecEd25519.d))
    (H:=Extended.point(F:=fe25519)(Feq:=ModularBaseSystem.eq))
    (EQ:=Logic.eq)(eq:=Extended.eq)
    (OP:=E.add(Fzero:=F.zero)(Fone:=F.one)(Fdiv:=F.div))
    (op:=Extended.add(Fadd:=GF25519.add)(Fmul:=GF25519.mul)(Fdiv:=ModularBaseSystem.div))
    .
(* Algebra.Group.is_homomorphism *)
(*      : Prop *)
(* where *)
(* ?Fzero : [Feq := ModularBaseSystem.eq *)
(*               : Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*                 Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*                 Prop |- fe25519]  *)
(* ?Fone : [Feq := ModularBaseSystem.eq *)
(*              : Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*                Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*                Prop |- fe25519]  *)
(* ?a : [Feq := ModularBaseSystem.eq *)
(*           : Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*             Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> Prop *)
(*      |- fe25519]  *)
(* ?d : [Feq := ModularBaseSystem.eq *)
(*           : Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*             Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> Prop *)
(*      |- fe25519]  *)
(* ?prm : [Feq := ModularBaseSystem.eq *)
(*             : Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*               Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> Prop *)
(*        |- E.twisted_edwards_params]  *)
(* ?Fopp : [Feq := ModularBaseSystem.eq *)
(*              : Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*                Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*                Prop |- fe25519 -> fe25519]  *)
(* ?Fsub : [Feq := ModularBaseSystem.eq *)
(*              : Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*                Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*                Prop |- fe25519 -> fe25519 -> fe25519]  *)
(* ?Finv : [Feq := ModularBaseSystem.eq *)
(*              : Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*                Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*                Prop |- fe25519 -> fe25519]  *)
(* ?field : [Feq := ModularBaseSystem.eq *)
(*               : Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*                 Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*                 Prop |- Algebra.field]  *)
(* ?prm0 : [Feq := ModularBaseSystem.eq *)
(*              : Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*                Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*                Prop |- E.twisted_edwards_params]  *)
(* ?a_eq_minus1 : [Feq := ModularBaseSystem.eq *)
(*                     : Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*                       Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*                       Prop |- ModularBaseSystem.eq ?a (?Fopp ?Fone)]  *)
(* ?twice_d : [Feq := ModularBaseSystem.eq *)
(*                 : Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*                   Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*                   Prop |- fe25519]  *)
(* ?Htwice_d : [Feq := ModularBaseSystem.eq *)
(*                  : Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*                    Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*                    Prop |- ModularBaseSystem.eq ?twice_d (add ?d ?d)]  *)
(* ?phi : [Feq := ModularBaseSystem.eq *)
(*             : Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> *)
(*               Tuple.tuple Z (length PseudoMersenneBaseParams.limb_widths) -> Prop *)
(*        |- E.point -> Extended.point]  *)