proposition: Lemma sqrt_invf (a :R) : (Num.sqrt(a))^-1 = Num.sqrt(a^-1).
proof: Proof. apply /eqP. case: (Num.sqrt a =P 0). move=> sqrt_a_eq0. by rewrite sqrt_a_eq0 eq_sym invr0 sqrtr_eq0 invr_le0 -sqrtr_eq0 sqrt_a_eq0. move=>/eqP sqrt_a_neq0. have: 0 < a by move: sqrt_a_neq0; rewrite sqrtr_eq0 -ltNge. move=> a_gt0. rewrite eq_sym -divf_eq1 ?invr_eq0 // invrK -sqrtrM ?invr_ge0 ?ltW //. rewrite mulrC divff ?sqrtr1 ?lt0r_neq0 //. 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