proposition: Lemma grada_distincts : forall A B C D E F, GradA A B C D E F -> A <> B /\ C <> B /\ D <> E /\ F <> E.
proof: Proof. induction 1. assert_diffs; repeat split; trivial. apply suma_distincts in H2; spliter; repeat split; auto. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.archimedes GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch12_parallel