proposition: Lemma cf_triangle_leif phi psi : sqrtC '[phi + psi] <= sqrtC '[phi] + sqrtC '[psi] ?= iff ~~ free (phi :: psi) && (0 <= coord [tuple psi] 0 phi).
proof: Proof. rewrite -(mono_in_leif ler_sqr) ?rpredD ?qualifE/= ?sqrtC_ge0 ?cfnorm_ge0 //; [| exact: O.. ]. rewrite andbC sqrrD !sqrtCK addrAC cfnormD (mono_leif (lerD2l _)). rewrite -mulr_natr -[_ + _](divfK (negbT (eqC_nat 2 0))) -/('Re _). rewrite (mono_leif (ler_pM2r _)) ?ltr0n //. have:= leif_trans (leif_Re_Creal '[phi, psi]) (cfCauchySchwarz_sqrt phi psi). congr (_ <= _ ?= iff _); first by rewrite ReE. apply: andb_id2r; rewrite free_cons span_seq1 seq1_free -negb_or negbK orbC /=. have [-> | nz_psi] := eqVneq psi 0; first by rewrite cfdot0r coord0. case/vlineP=> [x ->]; rewrite cfdotZl linearZ pmulr_lge0 ?cfnorm_gt0 //=. by rewrite (coord_free 0) ?seq1_free // eqxx mulr1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient finalg action gproduct) mathcomp(zmodp commutator cyclic center pgroup sylow) mathcomp(matrix vector falgebra ssrnum algC algnum) mathcomp(archimedean)