proposition: Lemma CReal_min_assoc : forall a b c : CReal, CReal_min a (CReal_min b c) == CReal_min (CReal_min a b) c.
proof: Proof. split. - apply CReal_min_glb. + apply (CReal_le_trans _ (CReal_min a b)). * apply CReal_min_l. * apply CReal_min_l. + apply CReal_min_glb. * apply (CReal_le_trans _ (CReal_min a b)). -- apply CReal_min_l. -- apply CReal_min_r. * apply CReal_min_r. - apply CReal_min_glb. + apply CReal_min_glb. * apply CReal_min_l. * apply (CReal_le_trans _ (CReal_min b c)). -- apply CReal_min_r. -- apply CReal_min_l. + apply (CReal_le_trans _ (CReal_min b c)). * apply CReal_min_r. * apply CReal_min_r. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra