proposition: Lemma max_comm : forall l r m, max l r m -> max r l m.
proof: Proof. intros. constructor. - apply H. - apply H. - intros. apply H; assumption. Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat