proposition: Lemma CRmax_assoc : forall {R : ConstructiveReals} (a b c : CRcarrier R), CRmax a (CRmax b c) == CRmax (CRmax a b) c.
proof: Proof. split. - apply CRmax_lub. + apply CRmax_lub. * apply CRmax_l. * apply (CRle_trans _ (CRmax b c)). -- apply CRmax_l. -- apply CRmax_r. + apply (CRle_trans _ (CRmax b c)). * apply CRmax_r. * apply CRmax_r. - apply CRmax_lub. + apply (CRle_trans _ (CRmax a b)). * apply CRmax_l. * apply CRmax_l. + apply CRmax_lub. * apply (CRle_trans _ (CRmax a b)). -- apply CRmax_r. -- apply CRmax_l. * apply CRmax_r. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs ConstructiveRealsMorphisms