proposition: Lemma mmax_inverse : forall `{Inhab A} (le:binary A) (P:A->Prop), mmax le P = mmin (inverse le) P.
proof: Proof. Proof using. intros. applys epsilon_eq. intros x. rewrite* max_element_inverse. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation LibOrder LibEpsilon)