proposition: Lemma min_assoc : forall a b c, forall bc, min b c bc -> forall ab, min a b ab -> forall abc, min a bc abc <-> min ab c abc.
proof: Proof. intros a b c bc BC ab AB abc. split; intros ABC. - constructor. + apply (min_greatest AB). * apply (min_l ABC). * rewrite (min_r ABC). apply (min_l BC). + rewrite (min_r ABC). apply (min_r BC). + intros. apply (min_greatest ABC). * rewrite H. apply (min_l AB). * apply (min_greatest BC). rewrite H. apply (min_r AB). assumption. - constructor. + rewrite (min_l ABC). apply (min_l AB). + apply (min_greatest BC). * rewrite (min_l ABC). apply (min_r AB). * apply (min_r ABC). + intros. apply (min_greatest ABC). * apply (min_greatest AB). assumption. rewrite H0. apply (min_l BC). * rewrite H0. apply (min_r BC). Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat