proposition: Lemma pisurtrois_triangle_utile2: forall a b c B C P, 0 < a -> 0 < b -> 0 < c -> (a + b) + c = pisurtrois -> B <> C -> B <> P -> image_angle b = cons_AV (vec B C) (vec B P) -> triangle B C P.
proof: Proof. intros. apply non_multiple_pi_triangle with b; auto. split. lra. rewrite <- pisurtrois_def. lra. Qed.