File: zagier.v

package info (click to toggle)
mathcomp-zify 1.5.0%2B2.0%2B8.16-4
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 228 kB
  • sloc: makefile: 43
file content (17 lines) | stat: -rw-r--r-- 468 bytes parent folder | download | duplicates (2) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
 
From mathcomp Require Import all_ssreflect zify.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma zagierK x y z : 0 < x -> 0 < z -> 
  let zagier t :=
    let: (x, y, z) := t in
    if x < y - z then (x + z.*2, z, y - z - x)
    else if x < y.*2 then (y.*2 - x, y, x + z - y)
    else (x - y.*2, x + z - y, y) in
  zagier (zagier (x, y, z)) = (x, y, z).
Proof.
move=> xP zP /=.
repeat case: leqP => *; congr (_,_,_); lia.
Qed.