gaxiiiiiiiiiiii

import Mathlib

lemma Subgroup.IsCyclic [Group G] [HG : IsCyclic G] (H : Subgroup G)  :
  IsCyclic H
:= by
  haveI := Classical.propDecidable
  obtain ⟨g, Hg : ∀ h, ∃ k, g ^ k = h⟩ := HG
  cases' subsingleton_or_nontrivial H with H0 H0
  · rcases H0 with ⟨H0⟩
    constructor; use 1; intro h; simp

gaxiiiiiiiiiiii

import Mathlib.tactic

example [Group G] [Fintype G] (g : G) :
  Fintype.card (Subgroup.zpowers g) = orderOf g
:= by
   have : orderOf g = Fintype.card (Fin (orderOf g)) := by simp
   rw [this]
   apply Fintype.card_congr
   refine {
    toFun := λ ⟨x, Hx⟩ => by

gaxiiiiiiiiiiii

import Mathlib.tactic
import Mathlib.GroupTheory.Complement

open Classical
open scoped Pointwise

lemma Subgroup.card_not_eq [Group G] [Fintype G] (H : Subgroup G) :
  Fintype.card ↑H ≠ 0
:= by
  intro F

gaxiiiiiiiiiiii

From mathcomp Require Import ssreflect.
Require Import Nat.

Definition name := nat.

Inductive proc :=
  | Nil
  | Tau (P : proc)
  | Para (P Q : proc)
  | Sum (P Q : proc)

gaxiiiiiiiiiiii

From mathcomp Require Import ssreflect.
From Autosubst Require Import Autosubst.
Require Import Nat.

Inductive proc_ :=
  | Var (x : var)
  | Nil
  | Para (P Q : proc_)
  | Repl (P : proc_)
  | Send (M : proc_) (N : proc_) (P : proc_)

gaxiiiiiiiiiiii

  function Pow(n:nat, k:nat) : (r:nat)
    ensures n > 0 ==> r > 0     
    {
        if k == 0 then 1
        else if k == 1 then n
        else
            var p := k / 2;
            var np := Pow(n,p);
            if p*2 == k then np * np
            else

gaxiiiiiiiiiiii

function Pow(n:nat, k:nat) : (r:nat)
  // Following needed for some proofs
  ensures n > 0 ==> r > 0     
  {
      if k == 0 then 1
      else if k == 1 then n
      else
          var p := k / 2;
          var np := Pow(n,p);
          if p*2 == k then np * np

gaxiiiiiiiiiiii

include "evm-dafny/src/dafny/core/memory.dfy"
include "evm-dafny/src/dafny/util/int.dfy"
include "evm-dafny/src/dafny/util/bytes.dfy"
include "evm-dafny/src/dafny/bytecode.dfy"
include "evm-dafny/src/dafny/evm.dfy"
// include "evm-dafny/libs/DafnyCrypto/src/dafny/util/math.dfy"

gaxiiiiiiiiiiii

datatype Expr =
  | Num(nat)
  | Add(Expr, Expr)
  | Mul(Expr, Expr)

function eval (e : Expr) : nat
{
  match e
  case Num(n) => n
  case Add(e1, e2) => eval(e1) + eval(e2)

gaxiiiiiiiiiiii

From UniMath Require Export MoreFoundations.All.
From UniMath Require Export OrderTheory.Posets.
From UniMath Require Export OrderTheory.DCPOs.
From DomainTheory Require Export Pataraia.
From mathcomp Require Export ssreflect.

Open Scope dcpo.
Open Scope subtype.
Open Scope logic.