proposition: Lemma one_quarter_lt_one_half: (1/(1+1)) * (1/(1+1)) < 1/(1+1) :> R.
proof: Proof. rewrite quarter ltr_pdivl_mulr ?addr_gt0 ?ltr01 //. rewrite mulrC mulrA ltr_pdivr_mulr ?addr_gt0 ?ltr01 //. rewrite mul1r mulr1 -subr_lt0 !opprD !addrA -[_+1-1]addrA subrr addr0. rewrite subrr add0r subr_lt0. by apply lt_trans with 0; first rewrite ltr_oppl; rewrite ?oppr0 ?ltr01. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype choice seq) mathcomp(fintype finset finfun bigop order) mathcomp(ssralg ssrnum path generic_quotient matrix mxalgebra algC) mathcomp(zmodp) GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.tarski_to_gupta_inspired GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Counter_models.Planar.independence