proposition: Lemma max_unique : forall l r m m' , PreO.max (le := leA) l r m -> PreO.max (le := leA) l r m' -> eqA m m'.
proof: Proof. intros. apply PO.le_antisym. - apply H; apply H0. - apply H0; apply H. Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat