Abhishek Anand aa755

## rewrite_drops_hyps.v
Require Import List.
Import ListNotations.
Require Import ssreflect.
Lemma test1 :
  length ([1] ++ [2]) = 2 ->
  2 = 4.
Proof.
  intros HA.
  evar (N : nat).
  Unshelve.

## fplbill.v
(** tries to reverse engineer FPL billing algorithm: given x watt consumption what should be the bill?
the bill is printed in cents.
it comes within 100cents in the test cases
but doesnt exactly match, even though all computations except the last one to print in decimal (error < 1 cent) are exact.
*)

Require Import QArith.
Require Import Coq.Classes.DecidableClass.
Definition Qmax (a b:Q) : Q :=
  if ((Qle_bool a b)) then b else a.

## gist:f7be3bf8116930fd935251a1650633ff
moved to https://aa755.github.io/decoding-human-body/ivermectin/2021/07/05/ivmrebuttal.html
	Require Import List.
	Import ListNotations.
	Require Import ssreflect.
	Lemma test1 :
	length ([1] ++ [2]) = 2 ->
	2 = 4.
	Proof.
	intros HA.
	evar (N : nat).
	Unshelve.
	(** tries to reverse engineer FPL billing algorithm: given x watt consumption what should be the bill?
	the bill is printed in cents.
	it comes within 100cents in the test cases
	but doesnt exactly match, even though all computations except the last one to print in decimal (error < 1 cent) are exact.
	*)

	Require Import QArith.
	Require Import Coq.Classes.DecidableClass.
	Definition Qmax (a b:Q) : Q :=
	if ((Qle_bool a b)) then b else a.