proposition: Theorem plus_id_exercise_from_basics : forall n m o : nat, n = m -> m = o -> n + m = m + o.
proof: Proof. Admitted. Theorem add_assoc_from_induction : forall n m p : nat, n + (m + p) = (n + m) + p. Proof. Admitted. Theorem S_injective_from_tactics : forall (n m : nat), S n = S m -> n = m. Proof. Admitted. Theorem or_distributes_over_and_from_logic : forall P Q R : Prop, P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R). Proof. Admitted. Example auto_example_1 : forall (P Q R: Prop), (P -> Q) -> (Q -> R) -> P -> R. Proof. intros P Q R H1 H2 H3. apply H2. apply H1. apply H3. Qed.
imports: Coq(Arith List) LF(IndProp) Coq(Lia)