| 67adfff | thery | 21 April 2021, 01:33:05 UTC | README | 21 April 2021, 01:33:05 UTC |
| 9010eb0 | thery | 21 April 2021, 01:15:30 UTC | update opam | 21 April 2021, 01:15:30 UTC |
| af77ae8 | thery | 21 April 2021, 00:52:43 UTC | opam instruction | 21 April 2021, 00:52:43 UTC |
| f48119f | thery | 08 February 2021, 08:34:55 UTC | update opam | 08 February 2021, 08:34:55 UTC |
| 0f7ab52 | thery | 08 February 2021, 08:32:40 UTC | update README | 08 February 2021, 08:32:40 UTC |
| d73f9bb | thery | 08 February 2021, 08:31:14 UTC | update README | 08 February 2021, 08:31:14 UTC |
| a23e54d | thery | 25 January 2021, 10:05:23 UTC | coq 8.13 | 25 January 2021, 10:05:23 UTC |
| 33beb81 | thery | 04 December 2020, 10:40:36 UTC | mathcomp 1.12 | 04 December 2020, 10:40:36 UTC |
| 0c753ce | thery | 27 August 2020, 01:43:55 UTC | opam 8.12 | 27 August 2020, 01:43:55 UTC |
| d490831 | thery | 27 August 2020, 00:51:01 UTC | coq 8.12 | 27 August 2020, 00:51:01 UTC |
| 20229a3 | thery | 23 July 2020, 09:58:33 UTC | hal ref | 23 July 2020, 09:58:33 UTC |
| 31b6ca3 | thery | 20 July 2020, 14:30:56 UTC | typo | 20 July 2020, 14:30:56 UTC |
| 2cdf93e | thery | 20 July 2020, 14:30:19 UTC | update readme | 20 July 2020, 14:30:19 UTC |
| b9e7102 | thery | 17 July 2020, 15:11:33 UTC | some renaming | 17 July 2020, 15:11:33 UTC |
| 4d42c52 | thery | 17 July 2020, 10:03:00 UTC | a[_,_] is better than z[_,_] | 17 July 2020, 10:03:00 UTC |
| e5665db | thery | 16 July 2020, 23:41:00 UTC | introduce the z[_,_] notation, remove all the case: odd | 16 July 2020, 23:41:00 UTC |
| 7f9a6fb | thery | 13 July 2020, 23:49:27 UTC | renaming | 13 July 2020, 23:49:27 UTC |
| 6c016d7 | thery | 12 July 2020, 22:43:08 UTC | typo | 12 July 2020, 22:43:08 UTC |
| e6c6be6 | thery | 11 July 2020, 13:18:58 UTC | hanoi -> rhanoi | 11 July 2020, 13:18:58 UTC |
| c3a1062 | thery | 11 July 2020, 11:14:31 UTC | refinement ppeg -> rpeg -> hanoi | 11 July 2020, 11:14:31 UTC |
| fdd196a | thery | 08 July 2020, 18:29:13 UTC | renaming | 08 July 2020, 18:29:13 UTC |
| 79cb2f8 | thery | 05 July 2020, 09:42:19 UTC | rm html2 | 05 July 2020, 09:42:19 UTC |
| 57b30eb | thery | 05 July 2020, 09:25:29 UTC | clean index | 05 July 2020, 09:25:29 UTC |
| acd116f | thery | 02 July 2020, 17:22:09 UTC | some html | 02 July 2020, 17:22:09 UTC |
| aae2dca | thery | 25 June 2020, 10:17:37 UTC | adopt the new style of induction with ubnP | 25 June 2020, 10:17:37 UTC |
| 2af2ab6 | thery | 25 June 2020, 08:38:27 UTC | fix shanoi4.v | 25 June 2020, 08:38:27 UTC |
| 7d5c852 | thery | 25 June 2020, 00:04:20 UTC | math-comp 1.11 | 25 June 2020, 00:04:20 UTC |
| e06848b | thery | 24 June 2020, 01:46:51 UTC | sp and sd functions | 24 June 2020, 01:46:51 UTC |
| abc5b6b | thery | 23 June 2020, 22:06:06 UTC | intensive use of ring | 23 June 2020, 22:06:06 UTC |
| f7cadfb | thery | 23 June 2020, 10:38:46 UTC | some refactoring | 23 June 2020, 10:38:46 UTC |
| 1db3092 | thery | 23 June 2020, 00:44:33 UTC | change tactic | 23 June 2020, 00:44:33 UTC |
| 2462121 | thery | 22 June 2020, 18:40:48 UTC | First version of the theorem gdist_S1 | 22 June 2020, 18:40:48 UTC |
| a088d56 | thery | 22 June 2020, 13:57:17 UTC | main proof done | 22 June 2020, 13:57:17 UTC |
| 1c23df1 | thery | 22 June 2020, 01:01:30 UTC | b=0 only case left | 22 June 2020, 01:01:30 UTC |
| c56f2e4 | thery | 21 June 2020, 22:11:58 UTC | b=1 and b=0 only cases left | 21 June 2020, 22:11:58 UTC |
| 088d35a | thery | 21 June 2020, 15:29:47 UTC | some simplification | 21 June 2020, 15:29:47 UTC |
| b5f6a29 | thery | 20 June 2020, 17:59:19 UTC | case a=c=1 in the box | 20 June 2020, 17:59:19 UTC |
| 15aa8dc | thery | 19 June 2020, 23:08:50 UTC | only easy cases left for a = c = 1 | 19 June 2020, 23:08:50 UTC |
| 7500b6a | thery | 19 June 2020, 00:28:56 UTC | separate the case where E is empty | 19 June 2020, 00:28:56 UTC |
| 824f42a | thery | 18 June 2020, 22:53:34 UTC | symmetry needed for case 2 between a and a1 | 18 June 2020, 22:53:34 UTC |
| d722614 | thery | 18 June 2020, 20:51:47 UTC | case a, b >=2 donne | 18 June 2020, 20:51:47 UTC |
| f830002 | thery | 18 June 2020, 14:58:13 UTC | b = 1 ok | 18 June 2020, 14:58:13 UTC |
| c2df8ff | thery | 18 June 2020, 01:26:44 UTC | case 2 : a, c >= 22 and b >= 2 ok | 18 June 2020, 01:26:44 UTC |
| 6410feb | thery | 17 June 2020, 18:04:17 UTC | all the sums are aligned in the first case of case 2 | 17 June 2020, 18:04:17 UTC |
| 44a7509 | thery | 17 June 2020, 15:36:21 UTC | some simplificatiobs | 17 June 2020, 15:36:21 UTC |
| 18f2506 | thery | 16 June 2020, 21:31:27 UTC | tiny progress | 16 June 2020, 21:31:27 UTC |
| beeb48e | thery | 15 June 2020, 21:43:58 UTC | tiny progress in case 2 | 15 June 2020, 21:43:58 UTC |
| 687e6ed | thery | 14 June 2020, 22:32:12 UTC | E empty in case 2 | 14 June 2020, 22:32:12 UTC |
| 4fac685 | thery | 14 June 2020, 18:57:28 UTC | Case 1 in the box | 14 June 2020, 18:57:28 UTC |
| a27227e | thery | 14 June 2020, 09:16:54 UTC | only case b = 0 left in case 1 | 14 June 2020, 09:16:54 UTC |
| d5cb50f | thery | 12 June 2020, 17:20:02 UTC | second subcase | 12 June 2020, 17:20:02 UTC |
| dd7006d | thery | 12 June 2020, 04:17:43 UTC | case a, b >= 2 of case 1 | 12 June 2020, 04:17:43 UTC |
| 1638b39 | thery | 11 June 2020, 21:42:47 UTC | fix | 11 June 2020, 21:42:47 UTC |
| 39fc0ce | thery | 11 June 2020, 21:34:27 UTC | some progress | 11 June 2020, 21:34:27 UTC |
| 6460f4b | thery | 10 June 2020, 21:26:19 UTC | first diagram | 10 June 2020, 21:26:19 UTC |
| c35ef0f | thery | 10 June 2020, 12:37:51 UTC | preliminary work for case 1 | 10 June 2020, 12:37:51 UTC |
| c030f0c | thery | 09 June 2020, 10:40:32 UTC | update readme | 09 June 2020, 10:40:32 UTC |
| 1c122e7 | thery | 09 June 2020, 01:31:18 UTC | starting 4.1 | 09 June 2020, 01:31:18 UTC |
| e08967b | thery | 08 June 2020, 00:26:39 UTC | 2.1 in the box | 08 June 2020, 00:26:39 UTC |
| 713c430 | thery | 06 June 2020, 23:46:36 UTC | connect shanoi | 06 June 2020, 23:47:55 UTC |
| 5d2035d | thery | 05 June 2020, 20:02:35 UTC | 3.7 | 05 June 2020, 20:02:35 UTC |
| 9f58a61 | thery | 05 June 2020, 18:54:43 UTC | 3.6 | 05 June 2020, 18:54:43 UTC |
| 9d32da0 | thery | 05 June 2020, 11:11:16 UTC | 3.5 | 05 June 2020, 11:11:16 UTC |
| b1cc964 | thery | 04 June 2020, 22:53:42 UTC | 3.4 in the box | 04 June 2020, 22:53:42 UTC |
| fd03ef2 | thery | 04 June 2020, 22:46:15 UTC | 3.4 in the box | 04 June 2020, 22:46:15 UTC |
| ae34a7a | thery | 04 June 2020, 20:43:02 UTC | 3.3 in the box | 04 June 2020, 20:43:02 UTC |
| 5e1bfd8 | thery | 02 June 2020, 18:22:08 UTC | tiny progress | 02 June 2020, 18:22:08 UTC |
| 45daf3d | thery | 02 June 2020, 13:41:52 UTC | sync with paper on S1 | 02 June 2020, 13:41:52 UTC |
| 1734395 | thery | 01 June 2020, 09:28:44 UTC | S[l] convex | 01 June 2020, 09:28:44 UTC |
| 52d4f26 | thery | 01 June 2020, 07:55:47 UTC | Notation | 01 June 2020, 07:55:47 UTC |
| 3e03f81 | thery | 31 May 2020, 22:38:32 UTC | convex conv | 31 May 2020, 22:38:32 UTC |
| 5b8f2fa | thery | 30 May 2020, 13:49:07 UTC | end section | 30 May 2020, 13:49:07 UTC |
| f2e073c | thery | 30 May 2020, 13:32:21 UTC | concave | 30 May 2020, 13:32:21 UTC |
| aa97410 | thery | 14 May 2020, 15:23:41 UTC | S -> 2 * S1 | 14 May 2020, 15:23:41 UTC |
| 194f783 | thery | 14 May 2020, 14:29:04 UTC | simplify fmerge proof | 14 May 2020, 14:29:04 UTC |
| e408c58 | thery | 14 May 2020, 12:45:08 UTC | starting with the star puzzle | 14 May 2020, 12:45:08 UTC |
| 3d669bd | thery | 04 May 2020, 15:28:23 UTC | Pdf | 04 May 2020, 15:28:23 UTC |
| 203ec50 | thery | 04 May 2020, 15:10:51 UTC | renaming | 04 May 2020, 15:10:51 UTC |
| c401246 | thery | 04 May 2020, 15:01:45 UTC | Note | 04 May 2020, 15:01:45 UTC |
| 0a4f4ca | thery | 04 May 2020, 14:51:10 UTC | some renaming | 04 May 2020, 14:51:10 UTC |
| a5859b5 | thery | 04 May 2020, 12:50:42 UTC | ghanoi4 + rm_rep | 04 May 2020, 12:50:42 UTC |
| 3cd4110 | thery | 04 May 2020, 08:47:48 UTC | Update doc | 04 May 2020, 08:47:48 UTC |
| f0ad68d | thery | 04 May 2020, 07:57:06 UTC | connectn | 04 May 2020, 07:57:06 UTC |
| 165e732 | thery | 29 April 2020, 16:24:42 UTC | type in README | 29 April 2020, 16:24:42 UTC |
| 85184fc | thery | 29 April 2020, 16:22:47 UTC | type in README | 29 April 2020, 16:22:47 UTC |
| bb9890d | thery | 29 April 2020, 16:10:21 UTC | update readme | 29 April 2020, 16:10:21 UTC |
| 1a0b0b0 | thery | 29 April 2020, 15:37:42 UTC | typo | 29 April 2020, 15:37:42 UTC |
| 4788bc7 | thery | 29 April 2020, 15:34:08 UTC | refactoring | 29 April 2020, 15:34:08 UTC |
| 194592c | thery | 29 April 2020, 14:15:16 UTC | in the box grep Axio *.v! | 29 April 2020, 14:15:16 UTC |
| 7a5eb50 | thery | 29 April 2020, 10:30:45 UTC | 2.9 in the box! | 29 April 2020, 10:30:45 UTC |
| af8bd36 | thery | 29 April 2020, 07:40:02 UTC | main inequality of the last case in the box | 29 April 2020, 07:40:02 UTC |
| d896ed2 | thery | 28 April 2020, 21:42:58 UTC | some progress | 28 April 2020, 21:42:58 UTC |
| 6d39e67 | thery | 27 April 2020, 08:45:04 UTC | one inequality missing | 27 April 2020, 08:45:04 UTC |
| f30bad0 | thery | 26 April 2020, 18:18:51 UTC | opam | 26 April 2020, 18:18:51 UTC |
| 8bf2116 | thery | 26 April 2020, 18:10:46 UTC | use of fset | 26 April 2020, 18:10:46 UTC |
| d430cf4 | thery | 25 April 2020, 05:44:04 UTC | one case left | 25 April 2020, 05:44:04 UTC |
| 616cd4a | thery | 23 April 2020, 23:10:46 UTC | case K = 0 | 23 April 2020, 23:10:46 UTC |
| 9225194 | thery | 22 April 2020, 07:42:22 UTC | geodesic | 22 April 2020, 07:42:22 UTC |
| 7049b02 | thery | 20 April 2020, 00:19:35 UTC | extend projection | 20 April 2020, 00:19:35 UTC |
| 7bad249 | thery | 19 April 2020, 18:36:14 UTC | refactoring | 19 April 2020, 18:36:14 UTC |
