fact: Definition funny_compare := fun x y => match (x,y) with | (inl x, inl y) => x < y | (inr x, inl y) => x <= y \/ x = (y+1)%nat | (inl x, inr y) => x + 2 <= y | (inr x, inr y) => x <= y end.
imports: Coq(Relations Lia) AlmostFull.PropBounded(AlmostFull) AlmostFull.PropBounded(AlmostFullInduction) AlmostFull.PropBounded(AFConstructions)