kik

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div choice fintype.
Require Import finfun path bigop.

Section Sec.
  Parameter n : nat.
  Parameter m : nat -> nat -> nat.
  Parameter mmax : nat -> nat.
  Parameter mmin : nat -> nat.
  Parameter right : nat -> nat.

kik

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div choice fintype.
Require Import finfun path fingraph bigop.

Section Sec.
  Parameter ch : finType.
  Parameter m : ch -> nat -> nat.
  Parameter right : ch -> ch.

  Parameter chpos : #|ch| > 0.
  Parameter meven0 : forall c, odd (m c 0) = false.

kik

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div fintype.
Require Import finfun path prime.

Theorem s2irr : forall n m, 2 * n ^ 2 = m ^ 2 -> n = 0 /\ m = 0.
Proof.
  move=> n m H.
  have: ~~((n > 0) && (m > 0)).
    apply/negP; case/andP => H1 H2.
    move/(congr1 (fun x => odd (logn 2 x))): H.
    by rewrite !logn_mul //= ?addnn ?odd_double ?expn_gt0 ?H1.

kik

Require Import Ascii String List Sorting Permutation PermutEq PermutSetoid.

Open Scope char_scope.

Definition trans := ascii -> ascii.

Definition chars : list ascii :=
  Eval compute in map ascii_of_nat (seq 0 256).

Definition smalls : list ascii :=

kik

#include <iostream>

using namespace std;

int main()
{
  int T;
  cin >> T;
  for (int cas = 1; cas <= T; cas++) {
    int N, S, p;

kik

#include <iostream>
#include <set>

using namespace std;

int main()
{
  int T;
  cin >> T;
  for (int cas = 1; cas <= T; cas++) {

kik

#include <iostream>
#include <vector>
#include <boost/math/common_factor.hpp>
#include <algorithm>

using namespace std;

typedef vector<vector<char> > room_t;

int main()

kik

#include <cstdio>
#include <cstring>
#include <algorithm>

using namespace std;

typedef unsigned char  u8;
typedef unsigned short u16;
typedef unsigned int   u32;

kik

int sc_rst = 2;

byte read_rst() {
  return digitalRead(sc_rst); 
}

void setup() {
  Serial.begin(9600);
  pinMode(sc_rst, INPUT);
  while (read_rst())

kik

#include <unistd.h>
#include <cstdlib>
#include <cstdio>
#include <vector>
#include <iostream>
#include <utility>
#include <string>
#include <random>
#include <memory>