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