proposition: Lemma CRmin_assoc : forall {R : ConstructiveReals} (a b c : CRcarrier R), CRmin a (CRmin b c) == CRmin (CRmin a b) c.
proof: Proof. split. - apply CRmin_glb. + apply (CRle_trans _ (CRmin a b)). * apply CRmin_l. * apply CRmin_l. + apply CRmin_glb. * apply (CRle_trans _ (CRmin a b)). -- apply CRmin_l. -- apply CRmin_r. * apply CRmin_r. - apply CRmin_glb. + apply CRmin_glb. * apply CRmin_l. * apply (CRle_trans _ (CRmin b c)). -- apply CRmin_r. -- apply CRmin_l. + apply (CRle_trans _ (CRmin b c)). * apply CRmin_r. * apply CRmin_r. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveAbs ConstructiveRealsMorphisms