fact: Definition at_most_one_upto (A : Type) (E : A -> A -> Prop) (P : A -> Prop) := forall x y, P x -> P y -> E x y.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)