proposition: Lemma CReal_max_assoc : forall a b c : CReal, CReal_max a (CReal_max b c) == CReal_max (CReal_max a b) c.
proof: Proof. split. - apply CReal_max_lub. + apply CReal_max_lub. * apply CReal_max_l. * apply (CReal_le_trans _ (CReal_max b c)). -- apply CReal_max_l. -- apply CReal_max_r. + apply (CReal_le_trans _ (CReal_max b c)). * apply CReal_max_r. * apply CReal_max_r. - apply CReal_max_lub. + apply (CReal_le_trans _ (CReal_max a b)). * apply CReal_max_l. * apply CReal_max_l. + apply CReal_max_lub. * apply (CReal_le_trans _ (CReal_max a b)). -- apply CReal_max_r. -- apply CReal_max_l. * apply CReal_max_r. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra